isColimit

Mathlib.CategoryTheory.Limits.VanKampen

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsUniversalColimit.isColimit

Lean4

/-- A universal colimit is a colimit. -/
noncomputable def isColimit {F : J ⥤ C} {c : Cocone F} (h : IsUniversalColimit c) : IsColimit c :=
  by
  refine
    ((h c (𝟙 F) (𝟙 c.pt :) (by rw [Functor.map_id, Category.comp_id, Category.id_comp])
          (NatTrans.equifibered_of_isIso _))
        fun j => ?_).some
  haveI : IsIso (𝟙 c.pt) := inferInstance
  exact IsPullback.of_vert_isIso ⟨by simp⟩

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

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

Разделы

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

Аффилиация

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