forgetCreatesColimitOfClosed

Mathlib.CategoryTheory.Limits.MorphismProperty

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

Lean4

/-- If `P` is closed under colimits of shape `J` in `Comma L R`, then when `D` has
a colimit in `Comma L R`, the forgetful functor creates this colimit. -/
noncomputable def forgetCreatesColimitOfClosed (h : ClosedUnderColimitsOfShape J (P.commaObj L R))
    [HasColimit (D ⋙ forget L R P ⊤ ⊤)] : CreatesColimit D (forget L R P ⊤ ⊤) :=
  createsColimitOfFullyFaithfulOfIso (⟨colimit (D ⋙ forget L R P ⊤ ⊤), h.colimit fun j ↦ (D.obj j).prop⟩) (Iso.refl _)

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

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

Разделы

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

Аффилиация

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