isColimit_iff_isIso_colimMap_ι — Mathlib

English

A cocone c is a colimit if and only if colimMap c.ι is an isomorphism (equivalently, there exists a colimit structure on c).

Русский

Кокон является ко-лимитом тогда и только тогда, когда colimMap c.ι является изоморфизмом (существует структура ко-лимита на c).

LaTeX

$$$\text{Nonempty}(\mathrm{IsColimit}(c)) \iff \mathrm{IsIso}(\mathrm{colimMap}(c.\iota))$$$

Lean4

theorem isColimit_iff_isIso_colimMap_ι {F : J ⥤ C} [HasColimit F] (c : Cocone F) :
    Nonempty (IsColimit c) ↔ IsIso (colimMap c.ι) :=
  ⟨fun ⟨h⟩ => IsColimit.isIso_colimMap_ι h, fun _ => ⟨c.isColimitOfIsIsoColimMapι⟩⟩

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