Creating (co)limits

We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

structure CategoryTheory.LiftableCone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) (c : Limits.Cone (K.comp F)) : Type (max (max (max u₁ v₁) v₂) w)

Define the lift of a cone: For a cone c for K ⋙ F, give a cone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of limits: every limit cone has a lift.

Note this definition is really only useful when c is a limit already.

• liftedCone : Limits.Cone K

  a cone in the source category of the functor

• validLift : F.mapCone self.liftedCone ≅ c

  the isomorphism expressing that liftedCone lifts the given cone

structure CategoryTheory.LiftableCocone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) (c : Limits.Cocone (K.comp F)) : Type (max (max (max u₁ v₁) v₂) w)

Define the lift of a cocone: For a cocone c for K ⋙ F, give a cocone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.

Note this definition is really only useful when c is a colimit already.

• liftedCocone : Limits.Cocone K

  a cocone in the source category of the functor

• validLift : F.mapCocone self.liftedCocone ≅ c

  the isomorphism expressing that liftedCocone lifts the given cocone

class CategoryTheory.CreatesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) extends CategoryTheory.Limits.ReflectsLimit K F : Type (max (max (max (max u₁ u₂) v₁) v₂) w)

Definition 3.3.1 of [Riehl]. We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

If F reflects isomorphisms, it suffices to show only that the lifted cone is a limit - see createsLimitOfReflectsIso.

• reflects {c : Cone K} (hc : IsLimit (F.mapCone c)) : Nonempty (IsLimit c)
• lifts (c : Limits.Cone (K.comp F)) : Limits.IsLimit c → LiftableCone K F c

  any limit cone can be lifted to a cone above

class CategoryTheory.CreatesLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

F creates limits of shape J if F creates the limit of any diagram K : J ⥤ C.

• CreatesLimit {K : Functor J C} : CategoryTheory.CreatesLimit K F

class CategoryTheory.CreatesLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

F creates limits if it creates limits of shape J for any J.

• CreatesLimitsOfShape {J : Type w} [Category.{w', w} J] : CategoryTheory.CreatesLimitsOfShape J F

@[reducible, inline]

abbrev CategoryTheory.CreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

F creates small limits if it creates limits of shape J for any small J.

Equations

• CategoryTheory.CreatesLimits F = CategoryTheory.CreatesLimitsOfSize.{?u.28, ?u.28, ?u.29, ?u.28, ?u.27, ?u.26} F

class CategoryTheory.CreatesColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) extends CategoryTheory.Limits.ReflectsColimit K F : Type (max (max (max (max u₁ u₂) v₁) v₂) w)

Dual of definition 3.3.1 of [Riehl]. We say that F creates colimits of K if, given any limit cocone c for K ⋙ F (i.e. below) we can lift it to a cocone "above", and further that F reflects limits for K.

If F reflects isomorphisms, it suffices to show only that the lifted cocone is a limit - see createsColimitOfReflectsIso.

• reflects {c : Cocone K} (hc : IsColimit (F.mapCocone c)) : Nonempty (IsColimit c)
• lifts (c : Limits.Cocone (K.comp F)) : Limits.IsColimit c → LiftableCocone K F c

  any limit cocone can be lifted to a cocone above

class CategoryTheory.CreatesColimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

F creates colimits of shape J if F creates the colimit of any diagram K : J ⥤ C.

• CreatesColimit {K : Functor J C} : CategoryTheory.CreatesColimit K F

class CategoryTheory.CreatesColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

F creates colimits if it creates colimits of shape J for any small J.

• CreatesColimitsOfShape {J : Type w} [Category.{w', w} J] : CategoryTheory.CreatesColimitsOfShape J F

@[reducible, inline]

abbrev CategoryTheory.CreatesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

F creates small colimits if it creates colimits of shape J for any small J.

Equations

• CategoryTheory.CreatesColimits F = CategoryTheory.CreatesColimitsOfSize.{?u.28, ?u.28, ?u.29, ?u.28, ?u.27, ?u.26} F

def CategoryTheory.liftLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesLimit K F] {c : Limits.Cone (K.comp F)} (t : Limits.IsLimit c) : Limits.Cone K

liftLimit t is the cone for K given by lifting the limit t for K ⋙ F.

Equations

• CategoryTheory.liftLimit t = (CategoryTheory.CreatesLimit.lifts c t).liftedCone

def CategoryTheory.liftedLimitMapsToOriginal {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesLimit K F] {c : Limits.Cone (K.comp F)} (t : Limits.IsLimit c) : F.mapCone (liftLimit t) ≅ c

The lifted cone has an image isomorphic to the original cone.

Equations

• CategoryTheory.liftedLimitMapsToOriginal t = (CategoryTheory.CreatesLimit.lifts c t).validLift

theorem CategoryTheory.liftedLimitMapsToOriginal_inv_map_π {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesLimit K F] {c : Limits.Cone (K.comp F)} (t : Limits.IsLimit c) (j : J) : CategoryStruct.comp (liftedLimitMapsToOriginal t).inv.hom (F.map ((liftLimit t).π.app j)) = c.π.app j

def CategoryTheory.liftedLimitIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesLimit K F] {c : Limits.Cone (K.comp F)} (t : Limits.IsLimit c) : Limits.IsLimit (liftLimit t)

The lifted cone is a limit.

Equations

• CategoryTheory.liftedLimitIsLimit t = CategoryTheory.Limits.isLimitOfReflects F (t.ofIsoLimit (CategoryTheory.liftedLimitMapsToOriginal t).symm)

theorem CategoryTheory.hasLimit_of_created {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [Limits.HasLimit (K.comp F)] [CreatesLimit K F] : Limits.HasLimit K

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

theorem CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (F : Functor C D) [Limits.HasLimitsOfShape J D] [CreatesLimitsOfShape J F] : Limits.HasLimitsOfShape J C

If F creates limits of shape J, and D has limits of shape J, then C has limits of shape J.

theorem CategoryTheory.hasLimits_of_hasLimits_createsLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.HasLimitsOfSize.{w, w', v₂, u₂} D] [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : Limits.HasLimitsOfSize.{w, w', v₁, u₁} C

If F creates limits, and D has all limits, then C has all limits.

def CategoryTheory.liftColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesColimit K F] {c : Limits.Cocone (K.comp F)} (t : Limits.IsColimit c) : Limits.Cocone K

liftColimit t is the cocone for K given by lifting the colimit t for K ⋙ F.

Equations

• CategoryTheory.liftColimit t = (CategoryTheory.CreatesColimit.lifts c t).liftedCocone

def CategoryTheory.liftedColimitMapsToOriginal {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesColimit K F] {c : Limits.Cocone (K.comp F)} (t : Limits.IsColimit c) : F.mapCocone (liftColimit t) ≅ c

The lifted cocone has an image isomorphic to the original cocone.

Equations

• CategoryTheory.liftedColimitMapsToOriginal t = (CategoryTheory.CreatesColimit.lifts c t).validLift

def CategoryTheory.liftedColimitIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [CreatesColimit K F] {c : Limits.Cocone (K.comp F)} (t : Limits.IsColimit c) : Limits.IsColimit (liftColimit t)

The lifted cocone is a colimit.

Equations

• CategoryTheory.liftedColimitIsColimit t = CategoryTheory.Limits.isColimitOfReflects F (t.ofIsoColimit (CategoryTheory.liftedColimitMapsToOriginal t).symm)

theorem CategoryTheory.hasColimit_of_created {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [Limits.HasColimit (K.comp F)] [CreatesColimit K F] : Limits.HasColimit K

If F creates the limit of K and K ⋙ F has a limit, then K has a limit.

theorem CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (F : Functor C D) [Limits.HasColimitsOfShape J D] [CreatesColimitsOfShape J F] : Limits.HasColimitsOfShape J C

If F creates colimits of shape J, and D has colimits of shape J, then C has colimits of shape J.

theorem CategoryTheory.hasColimits_of_hasColimits_createsColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.HasColimitsOfSize.{w, w', v₂, u₂} D] [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : Limits.HasColimitsOfSize.{w, w', v₁, u₁} C

If F creates colimits, and D has all colimits, then C has all colimits.

@[instance 10]

instance CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (F : Functor C D) [CreatesLimitsOfShape J F] : Limits.ReflectsLimitsOfShape J F

@[instance 10]

instance CategoryTheory.reflectsLimitsOfCreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

@[instance 10]

instance CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (F : Functor C D) [CreatesColimitsOfShape J F] : Limits.ReflectsColimitsOfShape J F

@[instance 10]

instance CategoryTheory.reflectsColimitsOfCreatesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

structure CategoryTheory.LiftsToLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) (c : Limits.Cone (K.comp F)) (t : Limits.IsLimit c) extends CategoryTheory.LiftableCone K F c : Type (max (max (max u₁ v₁) v₂) w)

A helper to show a functor creates limits. In particular, if we can show that for any limit cone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates limits. Usually, F creating limits says that any lift of c is a limit, but here we only need to show that our particular lift of c is a limit.

• liftedCone : Limits.Cone K
• validLift : F.mapCone self.liftedCone ≅ c
• makesLimit : Limits.IsLimit self.liftedCone

  the lifted cone is limit

structure CategoryTheory.LiftsToColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) (c : Limits.Cocone (K.comp F)) (t : Limits.IsColimit c) extends CategoryTheory.LiftableCocone K F c : Type (max (max (max u₁ v₁) v₂) w)

A helper to show a functor creates colimits. In particular, if we can show that for any limit cocone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates colimits. Usually, F creating colimits says that any lift of c is a colimit, but here we only need to show that our particular lift of c is a colimit.

• liftedCocone : Limits.Cocone K
• validLift : F.mapCocone self.liftedCocone ≅ c
• makesColimit : Limits.IsColimit self.liftedCocone

  the lifted cocone is colimit

def CategoryTheory.createsLimitOfReflectsIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] (h : (c : Limits.Cone (K.comp F)) → (t : Limits.IsLimit c) → LiftsToLimit K F c t) : CreatesLimit K F

If F reflects isomorphisms and we can lift any limit cone to a limit cone, then F creates limits. In particular here we don't need to assume that F reflects limits.

Equations

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

def CategoryTheory.createsLimitOfReflectsIso' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] {c : Limits.Cone (K.comp F)} (hc : Limits.IsLimit c) (h : LiftsToLimit K F c hc) : CreatesLimit K F

If F reflects isomorphisms and we can lift a single limit cone to a limit cone, then F creates limits. Note that unlike createsLimitOfReflectsIso, to apply this result it is necessary to know that K ⋙ F actually has a limit.

Equations

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

def CategoryTheory.createsLimitOfReflectsIsomorphismsOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] [Limits.HasLimit K] [Limits.PreservesLimit K F] : CreatesLimit K F

If F reflects isomorphisms, and we already know that the limit exists in the source and F preserves it, then F creates that limit.

Equations

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

def CategoryTheory.createsLimitOfFullyFaithfulOfLift' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] {l : Limits.Cone (K.comp F)} (hl : Limits.IsLimit l) (c : Limits.Cone K) (i : F.mapCone c ≅ l) : CreatesLimit K F

When F is fully faithful, to show that F creates the limit for K it suffices to exhibit a lift of a limit cone for K ⋙ F.

Equations

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

def CategoryTheory.createsLimitOfFullyFaithfulOfLift {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] [Limits.HasLimit (K.comp F)] (c : Limits.Cone K) (i : F.mapCone c ≅ Limits.limit.cone (K.comp F)) : CreatesLimit K F

When F is fully faithful, and HasLimit (K ⋙ F), to show that F creates the limit for K it suffices to exhibit a lift of the chosen limit cone for K ⋙ F.

Equations

• CategoryTheory.createsLimitOfFullyFaithfulOfLift c i = CategoryTheory.createsLimitOfFullyFaithfulOfLift' (CategoryTheory.Limits.limit.isLimit (K.comp F)) c i

def CategoryTheory.createsLimitOfFullyFaithfulOfIso' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] {l : Limits.Cone (K.comp F)} (hl : Limits.IsLimit l) (X : C) (i : F.obj X ≅ l.pt) : CreatesLimit K F

When F is fully faithful, to show that F creates the limit for K it suffices to show that a limit point is in the essential image of F.

Equations

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

def CategoryTheory.createsLimitOfFullyFaithfulOfIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] [Limits.HasLimit (K.comp F)] (X : C) (i : F.obj X ≅ Limits.limit (K.comp F)) : CreatesLimit K F

When F is fully faithful, and HasLimit (K ⋙ F), to show that F creates the limit for K it suffices to show that the chosen limit point is in the essential image of F.

Equations

• CategoryTheory.createsLimitOfFullyFaithfulOfIso X i = CategoryTheory.createsLimitOfFullyFaithfulOfIso' (CategoryTheory.Limits.limit.isLimit (K.comp F)) X i

def CategoryTheory.createsLimitOfFullyFaithfulOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] [Limits.HasLimit K] [Limits.PreservesLimit K F] : CreatesLimit K F

A fully faithful functor that preserves a limit that exists also creates the limit.

Equations

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

@[instance 100]

instance CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesLimit K F] [Limits.HasLimit (K.comp F)] : Limits.PreservesLimit K F

F preserves the limit of K if it creates the limit and K ⋙ F has the limit.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesLimit K F] [Limits.HasLimit (K.comp F)] : Limits.PreservesLimit K F

@[instance 100]

instance CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (F : Functor C D) [CreatesLimitsOfShape J F] [Limits.HasLimitsOfShape J D] : Limits.PreservesLimitsOfShape J F

F preserves the limit of shape J if it creates these limits and D has them.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

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

@[instance 100]

instance CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [Limits.HasLimitsOfSize.{w, w', v₂, u₂} D] : Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

F preserves limits if it creates limits and D has limits.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [Limits.HasLimitsOfSize.{w, w', v₂, u₂} D] : Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

def CategoryTheory.createsColimitOfReflectsIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] (h : (c : Limits.Cocone (K.comp F)) → (t : Limits.IsColimit c) → LiftsToColimit K F c t) : CreatesColimit K F

If F reflects isomorphisms and we can lift any colimit cocone to a colimit cocone, then F creates colimits. In particular here we don't need to assume that F reflects colimits.

Equations

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

def CategoryTheory.createsColimitOfReflectsIso' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] {c : Limits.Cocone (K.comp F)} (hc : Limits.IsColimit c) (h : LiftsToColimit K F c hc) : CreatesColimit K F

If F reflects isomorphisms and we can lift a single colimit cocone to a colimit cocone, then F creates limits. Note that unlike createsColimitOfReflectsIso, to apply this result it is necessary to know that K ⋙ F actually has a colimit.

Equations

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

def CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] [Limits.HasColimit K] [Limits.PreservesColimit K F] : CreatesColimit K F

If F reflects isomorphisms, and we already know that the colimit exists in the source and F preserves it, then F creates that colimit.

Equations

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

@[deprecated CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves (since := "2025-02-01")]

def CategoryTheory.createsColimitOfFullyFaithfulOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.ReflectsIsomorphisms] [Limits.HasColimit K] [Limits.PreservesColimit K F] : CreatesColimit K F

Alias of CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves.

---

If F reflects isomorphisms, and we already know that the colimit exists in the source and F preserves it, then F creates that colimit.

Equations

• @CategoryTheory.createsColimitOfFullyFaithfulOfPreserves = @CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves

def CategoryTheory.createsColimitOfFullyFaithfulOfLift' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] {l : Limits.Cocone (K.comp F)} (hl : Limits.IsColimit l) (c : Limits.Cocone K) (i : F.mapCocone c ≅ l) : CreatesColimit K F

When F is fully faithful, to show that F creates the colimit for K it suffices to exhibit a lift of a colimit cocone for K ⋙ F.

Equations

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

def CategoryTheory.createsColimitOfFullyFaithfulOfLift {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] [Limits.HasColimit (K.comp F)] (c : Limits.Cocone K) (i : F.mapCocone c ≅ Limits.colimit.cocone (K.comp F)) : CreatesColimit K F

When F is fully faithful, and HasColimit (K ⋙ F), to show that F creates the colimit for K it suffices to exhibit a lift of the chosen colimit cocone for K ⋙ F.

Equations

• CategoryTheory.createsColimitOfFullyFaithfulOfLift c i = CategoryTheory.createsColimitOfFullyFaithfulOfLift' (CategoryTheory.Limits.colimit.isColimit (K.comp F)) c i

def CategoryTheory.createsColimitOfFullyFaithfulOfIso' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] {l : Limits.Cocone (K.comp F)} (hl : Limits.IsColimit l) (X : C) (i : F.obj X ≅ l.pt) : CreatesColimit K F

When F is fully faithful, to show that F creates the colimit for K it suffices to show that a colimit point is in the essential image of F.

Equations

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

def CategoryTheory.createsColimitOfFullyFaithfulOfIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F : Functor C D} [F.Full] [F.Faithful] [Limits.HasColimit (K.comp F)] (X : C) (i : F.obj X ≅ Limits.colimit (K.comp F)) : CreatesColimit K F

When F is fully faithful, and HasColimit (K ⋙ F), to show that F creates the colimit for K it suffices to show that the chosen colimit point is in the essential image of F.

Equations

• CategoryTheory.createsColimitOfFullyFaithfulOfIso X i = CategoryTheory.createsColimitOfFullyFaithfulOfIso' (CategoryTheory.Limits.colimit.isColimit (K.comp F)) X i

@[instance 100]

instance CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesColimit K F] [Limits.HasColimit (K.comp F)] : Limits.PreservesColimit K F

F preserves the colimit of K if it creates the colimit and K ⋙ F has the colimit.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesColimit K F] [Limits.HasColimit (K.comp F)] : Limits.PreservesColimit K F

@[instance 100]

instance CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (F : Functor C D) [CreatesColimitsOfShape J F] [Limits.HasColimitsOfShape J D] : Limits.PreservesColimitsOfShape J F

F preserves the colimit of shape J if it creates these colimits and D has them.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

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

@[instance 100]

instance CategoryTheory.preservesColimits_of_createsColimits_and_hasColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [Limits.HasColimitsOfSize.{w, w', v₂, u₂} D] : Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

F preserves limits if it creates limits and D has limits.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [Limits.HasColimitsOfSize.{w, w', v₂, u₂} D] : Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

def CategoryTheory.createsLimitOfIsoDiagram {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K₁ K₂ : Functor J C} (F : Functor C D) (h : K₁ ≅ K₂) [CreatesLimit K₁ F] : CreatesLimit K₂ F

Transfer creation of limits along a natural isomorphism in the diagram.

Equations

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

def CategoryTheory.createsLimitOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F G : Functor C D} (h : F ≅ G) [CreatesLimit K F] : CreatesLimit K G

If F creates the limit of K and F ≅ G, then G creates the limit of K.

Equations

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

def CategoryTheory.createsLimitsOfShapeOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {F G : Functor C D} (h : F ≅ G) [CreatesLimitsOfShape J F] : CreatesLimitsOfShape J G

If F creates limits of shape J and F ≅ G, then G creates limits of shape J.

Equations

• CategoryTheory.createsLimitsOfShapeOfNatIso h = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.createsLimitOfNatIso h }

def CategoryTheory.createsLimitsOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F ≅ G) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

If F creates limits and F ≅ G, then G creates limits.

Equations

• CategoryTheory.createsLimitsOfNatIso h = { CreatesLimitsOfShape := fun {J : Type ?u.49} [CategoryTheory.Category.{?u.48, ?u.49} J] => CategoryTheory.createsLimitsOfShapeOfNatIso h }

def CategoryTheory.createsLimitsOfShapeOfEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {J' : Type w₁} [Category.{w'₁, w₁} J'] (e : J ≌ J') (F : Functor C D) [CreatesLimitsOfShape J F] : CreatesLimitsOfShape J' F

If F creates limits of shape J and J ≌ J', then F creates limits of shape J'.

Equations

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

def CategoryTheory.createsColimitOfIsoDiagram {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K₁ K₂ : Functor J C} (F : Functor C D) (h : K₁ ≅ K₂) [CreatesColimit K₁ F] : CreatesColimit K₂ F

Transfer creation of colimits along a natural isomorphism in the diagram.

Equations

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

def CategoryTheory.createsColimitOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {F G : Functor C D} (h : F ≅ G) [CreatesColimit K F] : CreatesColimit K G

If F creates the colimit of K and F ≅ G, then G creates the colimit of K.

Equations

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

def CategoryTheory.createsColimitsOfShapeOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {F G : Functor C D} (h : F ≅ G) [CreatesColimitsOfShape J F] : CreatesColimitsOfShape J G

If F creates colimits of shape J and F ≅ G, then G creates colimits of shape J.

Equations

• CategoryTheory.createsColimitsOfShapeOfNatIso h = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.createsColimitOfNatIso h }

def CategoryTheory.createsColimitsOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F ≅ G) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

If F creates colimits and F ≅ G, then G creates colimits.

Equations

• CategoryTheory.createsColimitsOfNatIso h = { CreatesColimitsOfShape := fun {J : Type ?u.49} [CategoryTheory.Category.{?u.48, ?u.49} J] => CategoryTheory.createsColimitsOfShapeOfNatIso h }

def CategoryTheory.createsColimitsOfShapeOfEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {J' : Type w₁} [Category.{w'₁, w₁} J'] (e : J ≌ J') (F : Functor C D) [CreatesColimitsOfShape J F] : CreatesColimitsOfShape J' F

If F creates colimits of shape J and J ≌ J', then F creates colimits of shape J'.

Equations

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

def CategoryTheory.liftsToLimitOfCreates {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesLimit K F] (c : Limits.Cone (K.comp F)) (t : Limits.IsLimit c) : LiftsToLimit K F c t

If F creates the limit of K, any cone lifts to a limit.

Equations

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

def CategoryTheory.liftsToColimitOfCreates {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesColimit K F] (c : Limits.Cocone (K.comp F)) (t : Limits.IsColimit c) : LiftsToColimit K F c t

If F creates the colimit of K, any cocone lifts to a colimit.

Equations

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

def CategoryTheory.idLiftsCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {K : Functor J C} (c : Limits.Cone (K.comp (Functor.id C))) : LiftableCone K (Functor.id C) c

Any cone lifts through the identity functor.

Equations

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

instance CategoryTheory.idCreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] : CreatesLimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (Functor.id C)

The identity functor creates all limits.

Equations

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

def CategoryTheory.idLiftsCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {K : Functor J C} (c : Limits.Cocone (K.comp (Functor.id C))) : LiftableCocone K (Functor.id C) c

Any cocone lifts through the identity functor.

Equations

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

instance CategoryTheory.idCreatesColimits {C : Type u₁} [Category.{v₁, u₁} C] : CreatesColimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (Functor.id C)

The identity functor creates all colimits.

Equations

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

instance CategoryTheory.inhabitedLiftableCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {K : Functor J C} (c : Limits.Cone (K.comp (Functor.id C))) : Inhabited (LiftableCone K (Functor.id C) c)

Satisfy the inhabited linter

Equations

• CategoryTheory.inhabitedLiftableCone c = { default := CategoryTheory.idLiftsCone c }

instance CategoryTheory.inhabitedLiftableCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type w} [Category.{w', w} J] {K : Functor J C} (c : Limits.Cocone (K.comp (Functor.id C))) : Inhabited (LiftableCocone K (Functor.id C) c)

Equations

• CategoryTheory.inhabitedLiftableCocone c = { default := CategoryTheory.idLiftsCocone c }

instance CategoryTheory.inhabitedLiftsToLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesLimit K F] (c : Limits.Cone (K.comp F)) (t : Limits.IsLimit c) : Inhabited (LiftsToLimit K F c t)

Satisfy the inhabited linter

Equations

• CategoryTheory.inhabitedLiftsToLimit K F c t = { default := CategoryTheory.liftsToLimitOfCreates K F c t }

instance CategoryTheory.inhabitedLiftsToColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [CreatesColimit K F] (c : Limits.Cocone (K.comp F)) (t : Limits.IsColimit c) : Inhabited (LiftsToColimit K F c t)

Equations

• CategoryTheory.inhabitedLiftsToColimit K F c t = { default := CategoryTheory.liftsToColimitOfCreates K F c t }

instance CategoryTheory.compCreatesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {E : Type u₃} [ℰ : Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesLimit K F] [CreatesLimit (K.comp F) G] : CreatesLimit K (F.comp G)

Equations

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

instance CategoryTheory.compCreatesLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {E : Type u₃} [ℰ : Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesLimitsOfShape J F] [CreatesLimitsOfShape J G] : CreatesLimitsOfShape J (F.comp G)

Equations

• CategoryTheory.compCreatesLimitsOfShape F G = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

instance CategoryTheory.compCreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [ℰ : Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [CreatesLimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : CreatesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)

Equations

• CategoryTheory.compCreatesLimits F G = { CreatesLimitsOfShape := fun {J : Type ?u.67} [CategoryTheory.Category.{?u.66, ?u.67} J] => inferInstance }

instance CategoryTheory.compCreatesColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {K : Functor J C} {E : Type u₃} [ℰ : Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesColimit K F] [CreatesColimit (K.comp F) G] : CreatesColimit K (F.comp G)

Equations

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

instance CategoryTheory.compCreatesColimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {E : Type u₃} [ℰ : Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesColimitsOfShape J F] [CreatesColimitsOfShape J G] : CreatesColimitsOfShape J (F.comp G)

Equations

• CategoryTheory.compCreatesColimitsOfShape F G = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

instance CategoryTheory.compCreatesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [ℰ : Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] [CreatesColimitsOfSize.{w, w', v₂, v₃, u₂, u₃} G] : CreatesColimitsOfSize.{w, w', v₁, v₃, u₁, u₃} (F.comp G)

Equations

• CategoryTheory.compCreatesColimits F G = { CreatesColimitsOfShape := fun {J : Type ?u.67} [CategoryTheory.Category.{?u.66, ?u.67} J] => inferInstance }