isColimitOfIsIsoColimMapι

Mathlib.CategoryTheory.Limits.Connected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cocone.isColimitOfIsIsoColimMapι

Lean4

/-- If `J` is connected, `F : J ⥤ C` and `C` is a cocone on `F`, then to check that `c` is a
colimit it is sufficient to check that `colimMap c.ι` is an isomorphism. The converse is also
true, see `Cocone.isColimit_iff_isIso_colimMap_ι`. -/
def isColimitOfIsIsoColimMapι {F : J ⥤ C} [HasColimit F] (c : Cocone F) [IsIso (colimMap c.ι)] : IsColimit c :=
  IsColimit.ofIsoColimit (colimit.isColimit _)
    (Cocones.ext (asIso (colimMap c.ι) ≪≫ (colimit.isColimit _).coconePointUniqueUpToIso (isColimitConstCocone J c.pt))
      (by simp))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru