hasLimit_of_closedUnderLimits — Mathlib

English

If J is a category and P is closed under limits of shape J, then F: J ⥤ P.FullSubcategory has a limit whenever F has a limit in the ambient category.

Русский

Если J — категория и P замкнута по пределам формы J, то любая диаграмма F: J ⥤ P.FullSubcategory имеет предел, если он есть в окружающей категории.

LaTeX

$$$[ClosedUnderLimitsOfShape J P] \\Rightarrow (F : J ⥤ P.FullSubcategory) [HasLimit (F \\circ P.ι)] \\Rightarrow HasLimit F$$$

Lean4

theorem hasLimit_of_closedUnderLimits (h : ClosedUnderLimitsOfShape J P) (F : J ⥤ P.FullSubcategory)
    [HasLimit (F ⋙ P.ι)] : HasLimit F :=
  have : CreatesLimit F P.ι := createsLimitFullSubcategoryInclusionOfClosed h F
  hasLimit_of_created F P.ι

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