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)

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 : CategoryTheory.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₁} [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)

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 : CategoryTheory.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₁} [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)

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 : 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

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')

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

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

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))

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

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

@[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.

Equations

• CategoryTheory.CreatesLimits F = CategoryTheory.CreatesLimitsOfSize.{v₂, v₂, v₁, v₂, u₁, u₂} F

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)

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 : 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

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')

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

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

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))

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

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

@[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.

Equations

• CategoryTheory.CreatesColimits F = CategoryTheory.CreatesColimitsOfSize.{v₂, v₂, v₁, v₂, u₁, u₂} F

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.liftedLimitIsLimit t = CategoryTheory.Limits.ReflectsLimit.reflects (CategoryTheory.Limits.IsLimit.ofIsoLimit t (CategoryTheory.liftedLimitMapsToOriginal t).symm)

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.liftedColimitIsColimit t = CategoryTheory.Limits.ReflectsColimit.reflects (CategoryTheory.Limits.IsColimit.ofIsoColimit t (CategoryTheory.liftedColimitMapsToOriginal t).symm)

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

Equations

• CategoryTheory.reflectsLimitsOfShapeOfCreatesLimitsOfShape F = { reflectsLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

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

Equations

• CategoryTheory.reflectsLimitsOfCreatesLimits F = { reflectsLimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => inferInstance }

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

Equations

• CategoryTheory.reflectsColimitsOfShapeOfCreatesColimitsOfShape F = { reflectsColimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

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

Equations

• CategoryTheory.reflectsColimitsOfCreatesColimits F = { reflectsColimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => inferInstance }

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)

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 : CategoryTheory.Limits.Cone K
• validLift : F.mapCone self.liftedCone ≅ c
• makesLimit : CategoryTheory.Limits.IsLimit self.liftedCone

  the lifted cone is 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)

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 : CategoryTheory.Limits.Cocone K
• validLift : F.mapCocone self.liftedCocone ≅ c
• makesColimit : CategoryTheory.Limits.IsColimit self.liftedCocone

  the lifted cocone is 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.

Equations

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

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] {c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp K F)} (hc : CategoryTheory.Limits.IsLimit c) (h : CategoryTheory.LiftsToLimit K F c hc) : CategoryTheory.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.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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

def CategoryTheory.createsLimitOfFullyFaithfulOfPreserves {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 K] [CategoryTheory.Limits.PreservesLimit K F] : CategoryTheory.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 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.

Equations

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

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.

Equations

• CategoryTheory.preservesLimitOfShapeOfCreatesLimitsOfShapeAndHasLimitsOfShape F = { preservesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

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.

Equations

• CategoryTheory.preservesLimitsOfCreatesLimitsAndHasLimits F = { preservesLimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => inferInstance }

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.

Equations

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

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] {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp K F)} (hc : CategoryTheory.Limits.IsColimit c) (h : CategoryTheory.LiftsToColimit K F c hc) : CategoryTheory.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.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.

Equations

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

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.

Equations

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

def CategoryTheory.createsColimitOfFullyFaithfulOfPreserves {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 K] [CategoryTheory.Limits.PreservesColimit K F] : CategoryTheory.CreatesColimit K F

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.preservesColimitOfShapeOfCreatesColimitsOfShapeAndHasColimitsOfShape F = { preservesColimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

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.

Equations

• CategoryTheory.preservesColimitsOfCreatesColimitsAndHasColimits F = { preservesColimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => inferInstance }

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.createsLimitsOfNatIso h = { CreatesLimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => CategoryTheory.createsLimitsOfShapeOfNatIso h }

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.createsColimitsOfNatIso h = { CreatesColimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => CategoryTheory.createsColimitsOfShapeOfNatIso h }

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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)

Equations

• CategoryTheory.inhabitedLiftableCocone c = { default := CategoryTheory.idLiftsCocone 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

Equations

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

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)

Equations

• CategoryTheory.inhabitedLiftsToColimit K F c t = { default := CategoryTheory.liftsToColimitOfCreates 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)

Equations

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

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)

Equations

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

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)

Equations

• CategoryTheory.compCreatesLimits F G = { CreatesLimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => inferInstance }

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)

Equations

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

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)

Equations

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

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)

Equations

• CategoryTheory.compCreatesColimits F G = { CreatesColimitsOfShape := fun {J : Type w'} [CategoryTheory.Category.{w, w'} J] => inferInstance }