isIso_π_of_isInitial — Mathlib

English

If I isInitial at j, then the projection π_F j is an isomorphism for any diagram F with a limit.

Русский

Если I является начальном в j, то проекция π_F j является изоморфизмом для любой диаграммы F с пределом.

LaTeX

$$$$\\forall j:\\, J,\\; (I:\\ IsInitial\\ j)\\Rightarrow \\mathrm{IsIso}(\\mathrm{limit}.\\pi F j).$$$$

Lean4

/-- If `j` is initial in the index category, then the map `limit.π F j` is an isomorphism.
-/
theorem isIso_π_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasLimit F] : IsIso (limit.π F j) :=
  ⟨⟨limit.lift _ (coneOfDiagramInitial I F), ⟨by ext; simp, by simp⟩⟩⟩

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