English
If all but one object in a diagram is strict terminal, then the limit is isomorphic to the said object via limit.π.
Русский
Если все, кроме одного, объектов диаграммы являются строгими терминальными, предел изоморфен этому объекту через limit.π.
LaTeX
$$$\text{IsIso}(\mathrm{limit.\\,\\pi} F i)$ under the condition $\forall j \neq i, \\ IsTerminal (F.obj j)$ and $[Subsingleton (i \\to i)]$$$
Lean4
/-- If all but one object in a diagram is strict terminal, then the limit is isomorphic to the
said object via `limit.π`. -/
theorem limit_π_isIso_of_is_strict_terminal (F : J ⥤ C) [HasLimit F] (i : J)
(H : ∀ (j) (_ : j ≠ i), IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : IsIso (limit.π F i) := by
classical
refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
· exact fun j => dite (j = i) (fun h => eqToHom (by cases h; rfl)) fun h => (H _ h).from _
· intro j k f
split_ifs with h h_1 h_1
· cases h
cases h_1
obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
simp
· cases h
haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
rw [← IsIso.comp_inv_eq]
apply (H _ h_1).hom_ext
· cases h_1
apply (H _ h).hom_ext
· apply (H _ h).hom_ext
· ext
rw [assoc, limit.lift_π]
dsimp only
split_ifs with h
· cases h
rw [id_comp, eqToHom_refl]
exact comp_id _
· apply (H _ h).hom_ext
· simp
