isIso_ι_terminal — Mathlib

English

If J has a terminal, then colimit.ι F (top J) is an isomorphism for any F with a colimit.

Русский

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

LaTeX

$$$$[HasTerminal\\ J]\\,(F: J \\to C)\\Rightarrow \\mathrm{IsIso}(\\mathrm{colimit}.\\ι F (\\top_J)).$$$$

Lean4

instance isIso_ι_terminal [HasTerminal J] (F : J ⥤ C) : IsIso (colimit.ι F (⊤_ J)) :=
  isIso_ι_of_isTerminal terminalIsTerminal F

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