# mathlibdocumentation

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} (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
• = ∀ ⦃F : J C⦄ ⦃c : ⦄, (∀ (j : J), P (F.obj j))P c.X
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
• = ∀ ⦃F : J C⦄ ⦃c : ⦄, (∀ (j : J), P (F.obj j))P c.X
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 )  :
theorem category_theory.limits.has_limits_of_shape_of_closed_under_limits {J : Type w} {C : Type u} {P : C → Prop}  :
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
noncomputable def category_theory.limits.creates_colimits_of_shape_full_subcategory_inclusion {J : Type w} {C : Type u} {P : C → Prop}  :

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

Equations
theorem category_theory.limits.has_colimit_of_closed_under_colimits {J : Type w} {C : Type u} {P : C → Prop} (F : J )  :
theorem category_theory.limits.has_colimits_of_shape_of_closed_under_colimits {J : Type w} {C : Type u} {P : C → Prop}  :