isIso_ι_of_isTerminal — Mathlib

English

If j is terminal in J, then the injections colimit.ι F j are isomorphisms for any diagram F with a colimit.

Русский

Если j терминальный в J, то инъекции colimit.ι F j являются изоморфизмами для любой диаграммы F с колимитом.

LaTeX

$$$$\\text{If } I:\\ IsTerminal\\ j,\\; F: J \\to C\\;\\Rightarrow\\; \\mathrm{IsIso}(\\mathrm{colimit}.\\ι F j).$$$$

Lean4

/-- If `j` is terminal in the index category, then the map `colimit.ι F j` is an isomorphism.
-/
theorem isIso_ι_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasColimit F] : IsIso (colimit.ι F j) :=
  ⟨⟨colimit.desc _ (coconeOfDiagramTerminal I F), ⟨by simp, by ext; simp⟩⟩⟩

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