# Documentation

Mathlib.CategoryTheory.Limits.Creates

# 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₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Type (max (max (max u₁ v₁) v₂) w)
• liftedCone :

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.

Instances For
structure CategoryTheory.LiftableCocone {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Type (max (max (max u₁ v₁) v₂) w)
• liftedCocone :

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.

Instances For
class CategoryTheory.CreatesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) extends :
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.

Instances
class CategoryTheory.CreatesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
• CreatesLimit : {K : } →

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

Instances
class CategoryTheory.CreatesLimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
• CreatesLimitsOfShape : {J : Type w} → [inst : ] →

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

Instances
@[inline, reducible]
abbrev CategoryTheory.CreatesLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
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.

Instances For
class CategoryTheory.CreatesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) extends :
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.

Instances
class CategoryTheory.CreatesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
• CreatesColimit : {K : } →

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

Instances
class CategoryTheory.CreatesColimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
• CreatesColimitsOfShape : {J : Type w} → [inst : ] →

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

Instances
@[inline, reducible]
abbrev CategoryTheory.CreatesColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
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.

Instances For
def CategoryTheory.liftLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :

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

Instances For
def CategoryTheory.liftedLimitMapsToOriginal {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :
F.mapCone () c

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

Instances For
def CategoryTheory.liftedLimitIsLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :

The lifted cone is a limit.

Instances For
theorem CategoryTheory.hasLimit_of_created {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

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₁} [] {D : Type u₂} [] {J : Type w} (F : ) :

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₁} [] {D : Type u₂} [] (F : ) [] [] :

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

def CategoryTheory.liftColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :

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

Instances For
def CategoryTheory.liftedColimitMapsToOriginal {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :
F.mapCocone () c

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

Instances For
def CategoryTheory.liftedColimitIsColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :

The lifted cocone is a colimit.

Instances For
theorem CategoryTheory.hasColimit_of_created {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

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

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₁} [] {D : Type u₂} [] (F : ) [] [] :

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

instance CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) :
instance CategoryTheory.reflectsLimitsOfCreatesLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :
instance CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) :
instance CategoryTheory.reflectsColimitsOfCreatesColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :
structure CategoryTheory.LiftsToLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) extends :
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.

Instances For
structure CategoryTheory.LiftsToColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) extends :
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.

Instances For
def CategoryTheory.createsLimitOfReflectsIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (h : (c : ) → (t : ) → ) :

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.

Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfLift' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (hl : ) (c : ) (i : F.mapCone c l) :

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.

Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfLift {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (c : ) (i : F.mapCone c ) :

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.

Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfIso' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (hl : ) (X : C) (i : F.obj X l.pt) :

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.

Instances For
def CategoryTheory.createsLimitOfFullyFaithfulOfIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (X : C) (i : F.obj X ) :

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.

Instances For
instance CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

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

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

instance CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] [] :

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

def CategoryTheory.createsColimitOfReflectsIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (h : (c : ) → (t : ) → ) :

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.

Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfLift' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (hl : ) (c : ) (i : F.mapCocone c l) :

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.

Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfLift {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (c : ) (i : F.mapCocone c ) :

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.

Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfIso' {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (hl : ) (X : C) (i : F.obj X l.pt) :

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.

Instances For
def CategoryTheory.createsColimitOfFullyFaithfulOfIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } (X : C) (i : ) :

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.

Instances For
instance CategoryTheory.preservesColimitOfCreatesColimitAndHasColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

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

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

instance CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] [] :

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

def CategoryTheory.createsLimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) [] :

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

Instances For
def CategoryTheory.createsLimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {G : } (h : F G) :

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

Instances For
def CategoryTheory.createsLimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

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

Instances For
def CategoryTheory.createsLimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

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

Instances For
def CategoryTheory.createsColimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) :

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

Instances For
def CategoryTheory.createsColimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {G : } (h : F G) :

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

Instances For
def CategoryTheory.createsColimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

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

Instances For
def CategoryTheory.createsColimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

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

Instances For
def CategoryTheory.liftsToLimitOfCreates {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

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

Instances For
def CategoryTheory.liftsToColimitOfCreates {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

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

Instances For
def CategoryTheory.idLiftsCone {C : Type u₁} [] {J : Type w} {K : } :

Any cone lifts through the identity functor.

Instances For
instance CategoryTheory.idCreatesLimits {C : Type u₁} [] :

The identity functor creates all limits.

def CategoryTheory.idLiftsCocone {C : Type u₁} [] {J : Type w} {K : } :

Any cocone lifts through the identity functor.

Instances For
instance CategoryTheory.idCreatesColimits {C : Type u₁} [] :

The identity functor creates all colimits.

instance CategoryTheory.inhabitedLiftableCone {C : Type u₁} [] {J : Type w} {K : } :

Satisfy the inhabited linter

instance CategoryTheory.inhabitedLiftableCocone {C : Type u₁} [] {J : Type w} {K : } :
instance CategoryTheory.inhabitedLiftsToLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

Satisfy the inhabited linter

instance CategoryTheory.inhabitedLiftsToColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
instance CategoryTheory.compCreatesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) :
instance CategoryTheory.compCreatesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
instance CategoryTheory.compCreatesLimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
instance CategoryTheory.compCreatesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) :
instance CategoryTheory.compCreatesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
instance CategoryTheory.compCreatesColimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :