opEquivOpOver — Mathlib

English

Dual statement: Under and Over are equivalent by reversing arrows.

Русский

Двойственное утверждение: Under и Over эквивалентны через обращение стрелок.

LaTeX

$$$\mathrm{Under.opEquivOpOver}(X): \mathrm{Under}(X) \simeq \mathrm{Over}(X)^{\mathrm{op}}$$$

Lean4

/-- The canonical equivalence between under and over categories by reversing structure arrows. -/
@[simps]
def opEquivOpOver : Under (op X) ≌ (Over X)ᵒᵖ
    where
  functor.obj Y := ⟨Over.mk Y.hom.unop⟩
  functor.map {Z Y} f := ⟨Over.homMk (f.right.unop) (by dsimp; rw [← unop_comp, Under.w])⟩
  inverse.obj Y := Under.mk (Y.unop.hom.op)
  inverse.map {Z Y} f := Under.homMk f.unop.left.op <| by dsimp; rw [← Over.w f.unop, op_comp]
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Похожие утверждения