# Limits in full subcategories #

We introduce the notion of a property closed under taking limits and show that if P is closed under taking limits, then limits in FullSubcategory P can be constructed from limits in C. More precisely, the inclusion creates such limits.

We say that a property is closed under limits of shape J if whenever all objects in a J-shaped diagram have the property, any limit of this diagram also has the property.

Equations
• = ∀ ⦃F : ⦄ ⦃c : ⦄, (∀ (j : J), P (F.obj j))P c.pt
Instances For

We say that a property is closed under colimits of shape J if whenever all objects in a J-shaped diagram have the property, any colimit of this diagram also has the property.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.ClosedUnderLimitsOfShape.limit {C : Type u} {J : Type w} {P : CProp} {F : } :
(∀ (j : J), P (F.obj j))
theorem CategoryTheory.Limits.ClosedUnderColimitsOfShape.colimit {C : Type u} {J : Type w} {P : CProp} {F : } :
(∀ (j : J), P (F.obj j))
def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' {J : Type w} {C : Type u} {P : CProp} {c : } (hc : ) (h : P c.pt) :

If a J-shaped diagram in FullSubcategory P has a limit cone in C whose cone point lives in the full subcategory, then this defines a limit in the full subcategory.

Equations
• One or more equations did not get rendered due to their size.
Instances For

If a J-shaped diagram in FullSubcategory P has a limit in C whose cone point lives in the full subcategory, then this defines a limit in the full subcategory.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion' {J : Type w} {C : Type u} {P : CProp} {c : } (hc : ) (h : P c.pt) :

If a J-shaped diagram in FullSubcategory P has a colimit cocone in C whose cocone point lives in the full subcategory, then this defines a colimit in the full subcategory.

Equations
• One or more equations did not get rendered due to their size.
Instances For

If a J-shaped diagram in FullSubcategory P has a colimit in C whose cocone point lives in the full subcategory, then this defines a colimit in the full subcategory.

Equations
• One or more equations did not get rendered due to their size.
Instances For

If P is closed under limits of shape J, then the inclusion creates such limits.

Equations
Instances For

If P is closed under limits of shape J, then the inclusion creates such limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated CategoryTheory.Limits.hasLimit_of_closedUnderLimits]

Alias of CategoryTheory.Limits.hasLimit_of_closedUnderLimits.

If P is closed under colimits of shape J, then the inclusion creates such colimits.

Equations
Instances For

If P is closed under colimits of shape J, then the inclusion creates such colimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated CategoryTheory.Limits.hasColimit_of_closedUnderColimits]

Alias of CategoryTheory.Limits.hasColimit_of_closedUnderColimits.

@[deprecated CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits]

Alias of CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits.