# mathlib3documentation

category_theory.limits.full_subcategory

# Limits in full subcategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} (J : Type w) (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
def category_theory.limits.closed_under_colimits_of_shape {C : Type u} (J : Type w) (P : C Prop) :
Prop

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
theorem category_theory.limits.closed_under_limits_of_shape.limit {C : Type u} {J : Type w} {P : C Prop} {F : J C}  :
( (j : J), P (F.obj j))
theorem category_theory.limits.closed_under_colimits_of_shape.colimit {C : Type u} {J : Type w} {P : C Prop} {F : J C}  :
( (j : J), P (F.obj j))
noncomputable def category_theory.limits.creates_limit_full_subcategory_inclusion' {J : Type w} {C : Type u} {P : C Prop} (F : J ) (h : P c.X) :

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
noncomputable def category_theory.limits.creates_limit_full_subcategory_inclusion {J : Type w} {C : Type u} {P : C Prop} (F : J )  :

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

Equations
noncomputable def category_theory.limits.creates_colimit_full_subcategory_inclusion' {J : Type w} {C : Type u} {P : C Prop} (F : J ) (h : P c.X) :

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
noncomputable def category_theory.limits.creates_colimit_full_subcategory_inclusion {J : Type w} {C : Type u} {P : C Prop} (F : J )  :

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

Equations
noncomputable def category_theory.limits.creates_limit_full_subcategory_inclusion_of_closed {J : Type w} {C : Type u} {P : C Prop} (F : J )  :

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

Equations
noncomputable def category_theory.limits.creates_limits_of_shape_full_subcategory_inclusion {J : Type w} {C : Type u} {P : C Prop}  :

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

Equations
theorem category_theory.limits.has_limit_of_closed_under_limits {J : Type w} {C : Type u} {P : C Prop} (F : J )  :
noncomputable def category_theory.limits.creates_colimit_full_subcategory_inclusion_of_closed {J : Type w} {C : Type u} {P : C Prop} (F : J )  :

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

Equations

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

Equations