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

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

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.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.toPrefunctor.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.toPrefunctor.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 (CategoryTheory.Functor.comp F (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 (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))] (h : P (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (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 (CategoryTheory.Functor.comp F (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 (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))] (h : P (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F (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 (CategoryTheory.Functor.comp F (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

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

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

• CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion h = CategoryTheory.CreatesLimitsOfShape.mk

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 (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasLimit F

theorem CategoryTheory.Limits.hasLimitsOfShape_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) [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 (CategoryTheory.Functor.comp F (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

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

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

• CategoryTheory.Limits.createsColimitsOfShapeFullSubcategoryInclusion h = CategoryTheory.CreatesColimitsOfShape.mk

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 (CategoryTheory.Functor.comp F (CategoryTheory.fullSubcategoryInclusion P))] : CategoryTheory.Limits.HasColimit F

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)