lift_self — Mathlib

English

Let F: J ⥤ C be a diagram and c a cone over F. If t is a limit cone for c, then the canonical self-map t.lift c equals the identity on c.pt.

Русский

Пусть F: J ⥤ C — диаграмма и c — конус над F. Если t является пределом конуса c, то канонический самоматрица t.lift c равна тождественному морфизму на вершине c.pt.

LaTeX

$$$ t.lift c = \\mathbb{1}_{c.pt} $$$

Lean4

@[simp]
theorem lift_self {c : Cone F} (t : IsLimit c) : t.lift c = 𝟙 c.pt :=
  (t.uniq _ _ fun _ => id_comp _).symm

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