desc_self — Mathlib

English

Let t be a cocone which is a colimit. Then the universal morphism from t to itself is the identity on its apex; i.e., the desc t equals the identity on t.pt.

Русский

Пусть t — кокон, являющийся колимитным. Тогда единственный универсальный морфизм от t к самому себе равен тождественному морфизму на вершине t.pt; тж. desc t = id_{t.pt}.

LaTeX

$$$ h.\mathrm{desc}\, t = 𝟙\ t.pt $$$

Lean4

@[simp]
theorem desc_self {t : Cocone F} (h : IsColimit t) : h.desc t = 𝟙 t.pt :=
  (h.uniq _ _ fun _ => comp_id _).symm

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