createsColimitFullSubcategoryInclusion

Mathlib.CategoryTheory.Limits.FullSubcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.createsColimitFullSubcategoryInclusion

Lean4

/-- If a `J`-shaped diagram in `FullSubcategory P` has a colimit in `C` whose cocone point lives in
    the full subcategory, then this defines a colimit in the full subcategory. -/
def createsColimitFullSubcategoryInclusion (F : J ⥤ P.FullSubcategory) [HasColimit (F ⋙ P.ι)]
    (h : P (colimit (F ⋙ P.ι))) : CreatesColimit F P.ι :=
  createsColimitFullSubcategoryInclusion' F (colimit.isColimit _) h

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

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

Разделы

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

Аффилиация

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