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 : ObjectProperty C) : 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.

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

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

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

def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (F : Functor J P.FullSubcategory) {c : Cone (F.comp P.ι)} (hc : IsLimit c) (h : P c.pt) : CreatesLimit F 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.

def CategoryTheory.Limits.createsLimitFullSubcategoryInclusion {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (F : Functor J P.FullSubcategory) [HasLimit (F.comp P.ι)] (h : P (limit (F.comp P.ι))) : CreatesLimit F 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.

def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion' {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (F : Functor J P.FullSubcategory) {c : Cocone (F.comp P.ι)} (hc : IsColimit c) (h : P c.pt) : CreatesColimit F 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.

def CategoryTheory.Limits.createsColimitFullSubcategoryInclusion {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (F : Functor J P.FullSubcategory) [HasColimit (F.comp P.ι)] (h : P (colimit (F.comp P.ι))) : CreatesColimit F 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.

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Limits.ClosedUnderLimitsOfShape.essImage {J : Type w} [Category.{w', w} J] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [HasLimitsOfShape J C] [PreservesLimitsOfShape J F] [F.Full] [F.Faithful] : ClosedUnderLimitsOfShape J F.essImage

The essential image of a functor is closed under the limits it preserves.

theorem CategoryTheory.Limits.ClosedUnderColimitsOfShape.essImage {J : Type w} [Category.{w', w} J] {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [HasColimitsOfShape J C] [PreservesColimitsOfShape J F] [F.Full] [F.Faithful] : ClosedUnderColimitsOfShape J F.essImage

The essential image of a functor is closed under the colimits it preserves.