hasLimitsOfShape_of_closedUnderLimits

English

If J is a shape and P is a property of objects in C closed under limits of shape J, and C has limits of shape J, then the full subcategory of C consisting of objects satisfying P has limits of shape J.

Русский

Пусть J — форма, P — свойство объектов в C, замкнутое относительно пределов формы J; если в C существуют пределы формы J, то соответствующая полная подпкатегория P.FullSubcategory имеет пределы формы J.

LaTeX

$$$\operatorname{HasLimitsOfShape}(J, C) \wedge \operatorname{ClosedUnderLimitsOfShape}(J, P) \Rightarrow \operatorname{HasLimitsOfShape}(J, P.FullSubcategory)$$$

Lean4

theorem hasLimitsOfShape_of_closedUnderLimits (h : ClosedUnderLimitsOfShape J P) [HasLimitsOfShape J C] :
    HasLimitsOfShape J P.FullSubcategory :=
  { has_limit := fun F => hasLimit_of_closedUnderLimits h F }

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