Limits in full subcategories

If a property of objects 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.

@[implicit_reducible]

noncomputable 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.

Equations

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

@[implicit_reducible]

noncomputable 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.

Equations

• CategoryTheory.Limits.createsLimitFullSubcategoryInclusion F h = CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' F (CategoryTheory.Limits.limit.isLimit (F.comp P.ι)) h

@[implicit_reducible]

noncomputable 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.

Equations

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

@[implicit_reducible]

noncomputable 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.

Equations

• CategoryTheory.Limits.createsColimitFullSubcategoryInclusion F h = CategoryTheory.Limits.createsColimitFullSubcategoryInclusion' F (CategoryTheory.Limits.colimit.isColimit (F.comp P.ι)) h

@[implicit_reducible]

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

Equations

• CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed J P F = CategoryTheory.Limits.createsLimitFullSubcategoryInclusion F ⋯

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion (J : Type w) [Category.{w', w} J] {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] [HasLimitsOfShape J C] : CreatesLimitsOfShape J 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 : ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] (F : Functor J P.FullSubcategory) [HasLimit (F.comp P.ι)] : HasLimit F

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

@[implicit_reducible]

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

Equations

• CategoryTheory.Limits.createsColimitFullSubcategoryInclusionOfClosed J P F = CategoryTheory.Limits.createsColimitFullSubcategoryInclusion F ⋯

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.createsColimitsOfShapeFullSubcategoryInclusion (J : Type w) [Category.{w', w} J] {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderColimitsOfShape J] [HasColimitsOfShape J C] : CreatesColimitsOfShape J 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 : ObjectProperty C) [P.IsClosedUnderColimitsOfShape J] (F : Functor J P.FullSubcategory) [HasColimit (F.comp P.ι)] : HasColimit F

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

theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (J : Type w) [Category.{w', w} J] [Limits.HasColimitsOfShape J P.FullSubcategory] [P.IsClosedUnderIsomorphisms] [Limits.PreservesColimitsOfShape J P.ι] : P.IsClosedUnderColimitsOfShape J

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (J : Type w) [Category.{w', w} J] [Limits.HasLimitsOfShape J P.FullSubcategory] [P.IsClosedUnderIsomorphisms] [Limits.PreservesLimitsOfShape J P.ι] : P.IsClosedUnderLimitsOfShape J

instance CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful {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] : F.essImage.IsClosedUnderLimitsOfShape J

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

instance CategoryTheory.Limits.instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful {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] : F.essImage.IsClosedUnderColimitsOfShape J

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