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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K F)) : Type (max (max (max u₁ v₁) v₂) w)

• liftedCone : CategoryTheory.Limits.Cone K

  a cone in the source category of the functor

• validLift : F.mapCone s.liftedCone ≅ c

  the isomorphism expressing that liftedCone lifts the given cone

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.

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

• liftedCocone : CategoryTheory.Limits.Cocone K

  a cocone in the source category of the functor

• validLift : F.mapCocone s.liftedCocone ≅ c

  the isomorphism expressing that liftedCocone lifts the given cocone

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.

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

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

  any limit cone can be lifted to a cone above

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.

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

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

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

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

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

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

@[inline, reducible]

abbrev CategoryTheory.CreatesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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.

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

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

  any limit cocone can be lifted to a cocone above

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.

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

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

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

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

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

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

@[inline, reducible]

abbrev CategoryTheory.CreatesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.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.

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

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

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

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

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

The lifted cone is a limit.

theorem CategoryTheory.hasLimit_of_created {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp K F)] [CategoryTheory.CreatesLimit K F] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.CreatesLimitsOfShape J F] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D] [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [CategoryTheory.CreatesColimit K F] {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp K F)} (t : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.Cocone K

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

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

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

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

The lifted cocone is a colimit.

theorem CategoryTheory.hasColimit_of_created {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp K F)] [CategoryTheory.CreatesColimit K F] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimitsOfShape J D] [CategoryTheory.CreatesColimitsOfShape J F] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D] [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} C

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

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

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

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

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

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

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

  the lifted cone is limit

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.

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

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

  the lifted cocone is colimit

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Any cone lifts through the identity functor.

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

The identity functor creates all limits.

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

Any cocone lifts through the identity functor.

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

The identity functor creates all colimits.

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

Satisfy the inhabited linter

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

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

Satisfy the inhabited linter

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

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

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

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

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

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

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