mathlib documentation

category_theory.limits.full_subcategory

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 full_subcategory P can be constructed from limits in C. More precisely, the inclusion creates such limits.

def category_theory.limits.closed_under_limits_of_shape {C : Type u} [category_theory.category C] (J : Type w) [category_theory.category J] (P : C → Prop) :
Prop

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

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

If a J-shaped diagram in full_subcategory 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

If a J-shaped diagram in full_subcategory 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