isColimitMapCoconeBinaryCofanEquiv

English

There is an equivalence between the statement that the mapped binary cofan is a colimit and that the mapped pair is a colimit.

Русский

Существует эквиваленция между тем, что отображённый бинарный ко-фан является колимит, и тем, что отображённая пара является колимит.

LaTeX

$$$IsColimit (Functor.mapCocone G (BinaryCofan.mk f g)) \simeq IsColimit (BinaryCofan.mk (G.map f) (G.map g))$$$

Lean4

/-- The map of a binary cofan is a colimit iff
the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `BinaryCofan.mk` with `Functor.mapCocone`.
-/
def isColimitMapCoconeBinaryCofanEquiv :
    IsColimit (Functor.mapCocone G (BinaryCofan.mk f g)) ≃ IsColimit (BinaryCofan.mk (G.map f) (G.map g)) :=
  (IsColimit.precomposeHomEquiv (diagramIsoPair _).symm _).symm.trans
    (IsColimit.equivIsoColimit (Cocones.ext (Iso.refl _) (by rintro (_ | _) <;> simp)))

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