costructuredArrowOpEquivalence — Mathlib

English

The left endpoint of F lies at the first object, i.e., left(F) = obj' F 0.

Русский

Левый конец F равен первому объекту: left(F) = obj' F 0.

LaTeX

$$$ \text{left}(F) = F.obj'\,0 $$$

Lean4

/-- For a functor `F : C ⥤ D` and an object `d : D`, the category of costructured arrows
`F.obj c ⟶ d` is contravariantly equivalent to the category of structured arrows
`op d ⟶ F.op.obj c`.
-/
def costructuredArrowOpEquivalence (F : C ⥤ D) (d : D) : (CostructuredArrow F d)ᵒᵖ ≌ StructuredArrow (op d) F.op
    where
  functor := CostructuredArrow.toStructuredArrow F d
  inverse := (StructuredArrow.toCostructuredArrow' F d).rightOp
  unitIso :=
    NatIso.ofComponents (fun X => (CostructuredArrow.isoMk (Iso.refl _)).op) fun {X Y} f =>
      Quiver.Hom.unop_inj <| by
        apply CommaMorphism.ext <;> dsimp [CostructuredArrow.isoMk, CostructuredArrow.homMk, Comma.isoMk]; simp
  counitIso :=
    NatIso.ofComponents (fun X => StructuredArrow.isoMk (Iso.refl _)) fun {X Y} f => by
      apply CommaMorphism.ext <;> dsimp [StructuredArrow.isoMk, StructuredArrow.homMk, Comma.isoMk]; simp

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