isIso_π_of_isTerminal — Mathlib

English

If j is terminal in J, then the projection π_F j is an isomorphism for any diagram F with a limit.

Русский

Если j является терминальным в J, то проекция π_F j является изоморфизмом.

LaTeX

$$$$\\text{If } I:\\ IsTerminal\\ j,\\; \\mathrm{HasLimit} F\\Rightarrow \\mathrm{IsIso}(\\mathrm{limit}.\\pi F j).$$$$

Lean4

theorem isIso_π_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasLimit F]
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (limit.π F j) :=
  ⟨⟨limit.lift _ (coneOfDiagramTerminal I F), by ext; simp, by simp⟩⟩

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