to_eq_descCoconeMorphism — Mathlib

English

Dually, the isInitial morphism recovers the to-s construction via the isColimit equivalence; i.e., hc.to s equals the described descCone morphism under the symmetry.

Русский

Дуально, изначальный морфизм восстанавливает конструкцию to s через эквивалентность isColimit; то есть hc.to s равно описанному descConemorphism через симметрию.

LaTeX

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

Lean4

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

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