desc_cocone — Mathlib

English

The desc from a cocone to its apex is the identity on the colimit when applied to the cocone itself.

Русский

desc для кокона возвращает тождественный морфизм на колимит, когда применяется к самому кокону.

LaTeX

$$$\\text{colimit.desc } F (\\text{colimit.cocone } F) = \\mathrm{Id}_{\\text{colimit } F}$$$

Lean4

@[simp]
theorem desc_cocone {F : J ⥤ C} [HasColimit F] : colimit.desc F (colimit.cocone F) = 𝟙 (colimit F) :=
  (colimit.isColimit _).desc_self

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