English
The canonical equivalence between over and under categories is given by reversing structure arrows.
Русский
Каноническая эквивалентность между Over и Under достигается обращением стрелок.
LaTeX
$$$\mathrm{opEquivOpUnder}(X): \mathrm{Over}(\mathrm{op}X) \simeq \mathrm{Under}(X)^{\mathrm{op}}$$$
Lean4
/-- The canonical equivalence between over and under categories by reversing structure arrows. -/
@[simps]
def opEquivOpUnder : Over (op X) ≌ (Under X)ᵒᵖ
where
functor.obj Y := ⟨Under.mk Y.hom.unop⟩
functor.map {Z Y} f := ⟨Under.homMk (f.left.unop) (by dsimp; rw [← unop_comp, Over.w])⟩
inverse.obj Y := Over.mk (Y.unop.hom.op)
inverse.map {Z Y} f := Over.homMk f.unop.right.op <| by dsimp; rw [← Under.w f.unop, op_comp]
unitIso := Iso.refl _
counitIso := Iso.refl _
