toCostructuredArrowIsoToCostructuredArrow

English

There is a canonical isomorphism expressing Functor.toCostructuredArrow in terms of Cocone.toCostructuredArrow, mirroring the structured-arrow case on the dual side.

Русский

Существуют канонические эквивалентности, выражающие Functor.toCostructuredArrow через Cocone.toCostructuredArrow, дуальный аналог ранее рассмотренного случая.

LaTeX

$$$G\\toCostructuredArrow F X f h \\cong (\\mathrm{Cocone.mk}\\; X\\; \\langle f, \\rangle).toCostructuredArrow \\circ \\mathrm{CostructuredArrow.pre}$$$

Lean4

/-- `Functor.toCostructuredArrow` can be expressed in terms of `Cocone.toCostructuredArrow`. -/
def _root_.CategoryTheory.Functor.toCostructuredArrowIsoToCostructuredArrow (G : J ⥤ K) (F : K ⥤ C) (X : C)
    (f : (Y : J) → F.obj (G.obj Y) ⟶ X) (h : ∀ {Y Z : J} (g : Y ⟶ Z), F.map (G.map g) ≫ f Z = f Y) :
    G.toCostructuredArrow F X f h ≅ (Cocone.mk X ⟨f, by simp [h]⟩).toCostructuredArrow ⋙ CostructuredArrow.pre _ _ _ :=
  Iso.refl _

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