mathlib3 documentation

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.

source
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
source
def category_theory.limits.closed_under_colimits_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 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
source
theorem category_theory.limits.closed_under_limits_of_shape.limit {C : Type u} [category_theory.category C] {J : Type w} [category_theory.category J] {P : C → Prop} (h : category_theory.limits.closed_under_limits_of_shape J P) {F : J ⥤ C} [category_theory.limits.has_limit F] :
(∀ (j : J), P (F.obj j)) → P (category_theory.limits.limit F)
source
theorem category_theory.limits.closed_under_colimits_of_shape.colimit {C : Type u} [category_theory.category C] {J : Type w} [category_theory.category J] {P : C → Prop} (h : category_theory.limits.closed_under_colimits_of_shape J P) {F : J ⥤ C} [category_theory.limits.has_colimit F] :
(∀ (j : J), P (F.obj j)) → P (category_theory.limits.colimit F)
source
noncomputable def category_theory.limits.creates_limit_full_subcategory_inclusion' {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (F : J ⥤ category_theory.full_subcategory P) {c : category_theory.limits.cone (F ⋙ category_theory.full_subcategory_inclusion P)} (hc : category_theory.limits.is_limit c) (h : P c.X) :
category_theory.creates_limit F (category_theory.full_subcategory_inclusion P)

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
source
noncomputable def category_theory.limits.creates_limit_full_subcategory_inclusion {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (F : J ⥤ category_theory.full_subcategory P) [category_theory.limits.has_limit (F ⋙ category_theory.full_subcategory_inclusion P)] (h : P (category_theory.limits.limit (F ⋙ category_theory.full_subcategory_inclusion P))) :
category_theory.creates_limit F (category_theory.full_subcategory_inclusion P)

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
source
noncomputable def category_theory.limits.creates_colimit_full_subcategory_inclusion' {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (F : J ⥤ category_theory.full_subcategory P) {c : category_theory.limits.cocone (F ⋙ category_theory.full_subcategory_inclusion P)} (hc : category_theory.limits.is_colimit c) (h : P c.X) :
category_theory.creates_colimit F (category_theory.full_subcategory_inclusion P)

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
source
noncomputable def category_theory.limits.creates_colimit_full_subcategory_inclusion {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (F : J ⥤ category_theory.full_subcategory P) [category_theory.limits.has_colimit (F ⋙ category_theory.full_subcategory_inclusion P)] (h : P (category_theory.limits.colimit (F ⋙ category_theory.full_subcategory_inclusion P))) :
category_theory.creates_colimit F (category_theory.full_subcategory_inclusion P)

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
source
noncomputable def category_theory.limits.creates_limit_full_subcategory_inclusion_of_closed {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_limits_of_shape J P) (F : J ⥤ category_theory.full_subcategory P) [category_theory.limits.has_limit (F ⋙ category_theory.full_subcategory_inclusion P)] :
category_theory.creates_limit F (category_theory.full_subcategory_inclusion P)

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

Equations
source
noncomputable def category_theory.limits.creates_limits_of_shape_full_subcategory_inclusion {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_limits_of_shape J P) [category_theory.limits.has_limits_of_shape J C] :
category_theory.creates_limits_of_shape J (category_theory.full_subcategory_inclusion P)

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

Equations
source
theorem category_theory.limits.has_limit_of_closed_under_limits {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_limits_of_shape J P) (F : J ⥤ category_theory.full_subcategory P) [category_theory.limits.has_limit (F ⋙ category_theory.full_subcategory_inclusion P)] :
category_theory.limits.has_limit F
source
theorem category_theory.limits.has_limits_of_shape_of_closed_under_limits {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_limits_of_shape J P) [category_theory.limits.has_limits_of_shape J C] :
category_theory.limits.has_limits_of_shape J (category_theory.full_subcategory P)
source
noncomputable def category_theory.limits.creates_colimit_full_subcategory_inclusion_of_closed {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_colimits_of_shape J P) (F : J ⥤ category_theory.full_subcategory P) [category_theory.limits.has_colimit (F ⋙ category_theory.full_subcategory_inclusion P)] :
category_theory.creates_colimit F (category_theory.full_subcategory_inclusion P)

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

Equations
source
noncomputable def category_theory.limits.creates_colimits_of_shape_full_subcategory_inclusion {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_colimits_of_shape J P) [category_theory.limits.has_colimits_of_shape J C] :
category_theory.creates_colimits_of_shape J (category_theory.full_subcategory_inclusion P)

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

Equations
source
theorem category_theory.limits.has_colimit_of_closed_under_colimits {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_colimits_of_shape J P) (F : J ⥤ category_theory.full_subcategory P) [category_theory.limits.has_colimit (F ⋙ category_theory.full_subcategory_inclusion P)] :
category_theory.limits.has_colimit F
source
theorem category_theory.limits.has_colimits_of_shape_of_closed_under_colimits {J : Type w} [category_theory.category J] {C : Type u} [category_theory.category C] {P : C → Prop} (h : category_theory.limits.closed_under_colimits_of_shape J P) [category_theory.limits.has_colimits_of_shape J C] :
category_theory.limits.has_colimits_of_shape J (category_theory.full_subcategory P)