descCoconeMorphism_eq_isInitial_to

English

The morphism descCoconeMorphism for a colimit cocone corresponds to the initial structure via isColimitEquivIsInitial; i.e., it equals the initial morphism expressed through the equivalence.

Русский

Морфизм descCoconeMorphism коллимитного кокона соответствует инциалу через isColimitEquivIsInitial.

LaTeX

$$$\\mathrm{descCoconeMorphism}(s) = \\mathrm{IsInitial.to} (\\mathrm{Cocone.isColimitEquivIsInitial}\\; _\\; hc)\\; s$$$

Lean4

theorem descCoconeMorphism_eq_isInitial_to {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (s : Cocone F) :
    hc.descCoconeMorphism s = IsInitial.to (Cocone.isColimitEquivIsInitial _ hc) _ :=
  rfl

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