structuredArrowOpEquivalence — Mathlib

English

Definition of a contravariant functor that assigns to each costructured-arrow object over F.op (op d) a structured arrow object from d to F.op, given by mapping objects and morphisms accordingly.

Русский

Определение контравариантного функторa, отображающего каждый объект CostructuredArrow F.op (op d) в структурированную стрелу d ⟶ F.op соответствующим преобразованием.

LaTeX

$$$$ \text{toStructuredArrow}'(F,d) \;:\; (\text{CostructuredArrow } F^{op} (op d))^{op} \to \text{StructuredArrow } d F.$$$$

Lean4

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

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