createsLimitFullSubcategoryInclusionOfClosed

Mathlib.CategoryTheory.Limits.FullSubcategory

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

Lean4

/-- If `P` is closed under limits of shape `J`, then the inclusion creates such limits. -/
def createsLimitFullSubcategoryInclusionOfClosed (h : ClosedUnderLimitsOfShape J P) (F : J ⥤ P.FullSubcategory)
    [HasLimit (F ⋙ P.ι)] : CreatesLimit F P.ι :=
  createsLimitFullSubcategoryInclusion F (h.limit fun j => (F.obj j).property)

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

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

Разделы

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

Аффилиация

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