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} [Category.{v, u} C] (J : Type w) [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} [Category.{v, u} C] (J : Type w) [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} [Category.{v, u} C] {J : Type w} [Category.{w', w} J] {P : C → Prop} [ClosedUnderIsomorphisms P] (h : ∀ {F : Functor J C} [inst : HasLimit F], (∀ (j : J), P (F.obj j)) → P (limit F)) : ClosedUnderLimitsOfShape J P

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

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

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

def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (F : Functor J (FullSubcategory P)) {c : Cone (F.comp (fullSubcategoryInclusion P))} (hc : IsLimit c) (h : P c.pt) : CreatesLimit F (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (F : Functor J (FullSubcategory P)) [HasLimit (F.comp (fullSubcategoryInclusion P))] (h : P (limit (F.comp (fullSubcategoryInclusion P)))) : CreatesLimit F (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (F : Functor J (FullSubcategory P)) {c : Cocone (F.comp (fullSubcategoryInclusion P))} (hc : IsColimit c) (h : P c.pt) : CreatesColimit F (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (F : Functor J (FullSubcategory P)) [HasColimit (F.comp (fullSubcategoryInclusion P))] (h : P (colimit (F.comp (fullSubcategoryInclusion P)))) : CreatesColimit F (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (h : ClosedUnderLimitsOfShape J P) (F : Functor J (FullSubcategory P)) [HasLimit (F.comp (fullSubcategoryInclusion P))] : CreatesLimit F (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (h : ClosedUnderLimitsOfShape J P) [HasLimitsOfShape J C] : CreatesLimitsOfShape J (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (h : ClosedUnderLimitsOfShape J P) (F : Functor J (FullSubcategory P)) [HasLimit (F.comp (fullSubcategoryInclusion P))] : HasLimit F

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

def CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (h : ClosedUnderColimitsOfShape J P) (F : Functor J (FullSubcategory P)) [HasColimit (F.comp (fullSubcategoryInclusion P))] : CreatesColimit F (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (h : ClosedUnderColimitsOfShape J P) [HasColimitsOfShape J C] : CreatesColimitsOfShape J (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} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : C → Prop} (h : ClosedUnderColimitsOfShape J P) (F : Functor J (FullSubcategory P)) [HasColimit (F.comp (fullSubcategoryInclusion P))] : HasColimit F

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