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.

def CategoryTheory.Limits.ClosedUnderLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{w', w} 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

• CategoryTheory.Limits.ClosedUnderLimitsOfShape J P = ∀ ⦃F : CategoryTheory.Functor J C⦄ ⦃c : CategoryTheory.Limits.Cone F⦄, CategoryTheory.Limits.IsLimit c → (∀ (j : J), P (F.obj j)) → P c.pt

def CategoryTheory.Limits.ClosedUnderColimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{w', w} 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

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

theorem CategoryTheory.Limits.closedUnderLimitsOfShape_of_limit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {P : C → Prop} [CategoryTheory.ClosedUnderIsomorphisms P] (h : ∀ {F : CategoryTheory.Functor J C} [inst : CategoryTheory.Limits.HasLimit F], (∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.limit F)) : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P

theorem CategoryTheory.Limits.closedUnderColimitsOfShape_of_colimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {P : C → Prop} [CategoryTheory.ClosedUnderIsomorphisms P] (h : ∀ {F : CategoryTheory.Functor J C} [inst : CategoryTheory.Limits.HasColimit F], (∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.colimit F)) : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P

theorem CategoryTheory.Limits.ClosedUnderLimitsOfShape.limit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasLimit F] : (∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.limit F)

theorem CategoryTheory.Limits.ClosedUnderColimitsOfShape.colimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) {F : CategoryTheory.Functor J C} [CategoryTheory.Limits.HasColimit F] : (∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.colimit F)

def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) {c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.fullSubcategoryInclusion P))} (hc : CategoryTheory.Limits.IsLimit c) (h : P c.pt) : CategoryTheory.CreatesLimit F (CategoryTheory.fullSubcategoryInclusion P)

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.

def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] (h : P (CategoryTheory.Limits.limit (F.comp (CategoryTheory.fullSubcategoryInclusion P)))) : CategoryTheory.CreatesLimit F (CategoryTheory.fullSubcategoryInclusion P)

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.

def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion' {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.fullSubcategoryInclusion P))} (hc : CategoryTheory.Limits.IsColimit c) (h : P c.pt) : CategoryTheory.CreatesColimit F (CategoryTheory.fullSubcategoryInclusion P)

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.

def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] (h : P (CategoryTheory.Limits.colimit (F.comp (CategoryTheory.fullSubcategoryInclusion P)))) : CategoryTheory.CreatesColimit F (CategoryTheory.fullSubcategoryInclusion P)

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.

def CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.CreatesLimit F (CategoryTheory.fullSubcategoryInclusion P)

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

Equations

• CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed h F = CategoryTheory.Limits.createsLimitFullSubcategoryInclusion F ⋯

def CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.fullSubcategoryInclusion P)

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.

theorem CategoryTheory.Limits.hasLimit_of_closedUnderLimits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasLimit F

@[deprecated CategoryTheory.Limits.hasLimit_of_closedUnderLimits]

theorem CategoryTheory.Limits.hasLimit_of_closed_under_limits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasLimit F

Alias of CategoryTheory.Limits.hasLimit_of_closedUnderLimits.

theorem CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P) [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.FullSubcategory P)

def CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.CreatesColimit F (CategoryTheory.fullSubcategoryInclusion P)

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

Equations

• CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed h F = CategoryTheory.Limits.createsColimitFullSubcategoryInclusion F ⋯

def CategoryTheory.Limits.createsColimitsOfShapeFullSubcategoryInclusion {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.fullSubcategoryInclusion P)

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.

theorem CategoryTheory.Limits.hasColimit_of_closedUnderColimits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasColimit F

@[deprecated CategoryTheory.Limits.hasColimit_of_closedUnderColimits]

theorem CategoryTheory.Limits.hasColimit_of_closed_under_colimits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) (F : CategoryTheory.Functor J (CategoryTheory.FullSubcategory P)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasColimit F

Alias of CategoryTheory.Limits.hasColimit_of_closedUnderColimits.

theorem CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.FullSubcategory P)

@[deprecated CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits]

theorem CategoryTheory.Limits.hasColimitsOfShape_of_closed_under_colimits {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C → Prop} (h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P) [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.FullSubcategory P)

Alias of CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits.