colimitsOfShape

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.colimitsOfShape

Lean4

/-- The class of morphisms in `C` that are colimits of shape `J` of
natural transformations involving morphisms in `W`. -/
inductive colimitsOfShape : MorphismProperty C
  |
  mk (X₁ X₂ : J ⥤ C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₂ : IsColimit c₂) (f : X₁ ⟶ X₂)
    (_ : W.functorCategory J f) : colimitsOfShape (h₁.desc (Cocone.mk _ (f ≫ c₂.ι)))

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

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

Разделы

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

Аффилиация

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