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.
Define the lift of a cone: For a cone c for K ⋙ F, give a cone for K
which is a lift of c, i.e. the image of it under F is (iso) to c.
We will then use this as part of the definition of creation of limits: every limit cone has a lift.
Note this definition is really only useful when c is a limit already.
- liftedCone : Limits.Cone K
a cone in the source category of the functor
the isomorphism expressing that
liftedConelifts the given cone
Instances For
Define the lift of a cocone: For a cocone c for K ⋙ F, give a cocone for
K which is a lift of c, i.e. the image of it under F is (iso) to c.
We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.
Note this definition is really only useful when c is a colimit already.
- liftedCocone : Limits.Cocone K
a cocone in the source category of the functor
the isomorphism expressing that
liftedCoconelifts the given cocone
Instances For
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.
- lifts (c : Limits.Cone (K.comp F)) : Limits.IsLimit c → LiftableCone K F c
any limit cone can be lifted to a cone above
F creates limits of shape J if F creates the limit of any diagram
K : J ⥤ C.
- CreatesLimit {K : Functor J C} : CategoryTheory.CreatesLimit K F
F creates limits if it creates limits of shape J for any J.
F creates small limits if it creates limits of shape J for any small J.
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.
- lifts (c : Limits.Cocone (K.comp F)) : Limits.IsColimit c → LiftableCocone K F c
any limit cocone can be lifted to a cocone above
F creates colimits of shape J if F creates the colimit of any diagram
K : J ⥤ C.
- CreatesColimit {K : Functor J C} : CategoryTheory.CreatesColimit K F
F creates colimits if it creates colimits of shape J for any small J.
- CreatesColimitsOfShape {J : Type w} [Category.{w', w} J] : CategoryTheory.CreatesColimitsOfShape J F
F creates small colimits if it creates colimits of shape J for any small J.
liftLimit t is the cone for K given by lifting the limit t for K ⋙ F.
Equations
The lifted cone has an image isomorphic to the original cone.
The lifted cone is a limit.
If F creates the limit of K and K ⋙ F has a limit, then K has a limit.
If F creates limits of shape J, and D has limits of shape J, then
C has limits of shape J.
If F creates limits, and D has all limits, then C has all limits.
liftColimit t is the cocone for K given by lifting the colimit t for K ⋙ F.
Equations
The lifted cocone has an image isomorphic to the original cocone.
The lifted cocone is a colimit.
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.
If F creates colimits, and D has all colimits, then C has all colimits.
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.
- makesLimit : Limits.IsLimit self.liftedCone
the lifted cone is limit
Instances For
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.
- makesColimit : Limits.IsColimit self.liftedCocone
the lifted cocone is colimit
Instances For
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
- CategoryTheory.createsLimitOfReflectsIso h = CategoryTheory.CreatesLimit.mk fun (c : CategoryTheory.Limits.Cone (K.comp F)) (t : CategoryTheory.Limits.IsLimit c) => (h c t).toLiftableCone
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.
If F reflects isomorphisms, and we already know that the limit exists in the source and F
preserves it, then F creates that limit.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
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.
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.
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.
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.
F preserves limits if it creates limits and D has limits.
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.
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.
If F reflects isomorphisms, and we already know that the colimit exists in the source and F
preserves it, then F creates that colimit.
Equations
- One or more equations did not get rendered due to their size.
Alias of CategoryTheory.createsColimitOfReflectsIsomorphismsOfPreserves.
If F reflects isomorphisms, and we already know that the colimit exists in the source and F
preserves it, then F creates that colimit.
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.
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.
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.
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.
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.
F preserves limits if it creates limits and D has limits.
Transfer creation of limits along a natural isomorphism in the diagram.
Equations
- One or more equations did not get rendered due to their size.
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.
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 }
If F creates limits and F ≅ G, then G creates limits.
Equations
- CategoryTheory.createsLimitsOfNatIso h = { CreatesLimitsOfShape := fun {J : Type ?u.68} [CategoryTheory.Category.{?u.67, ?u.68} J] => CategoryTheory.createsLimitsOfShapeOfNatIso h }
If F creates limits of shape J and J ≌ J', then F creates limits of shape J'.
Equations
- One or more equations did not get rendered due to their size.
Transfer creation of colimits along a natural isomorphism in the diagram.
Equations
- One or more equations did not get rendered due to their size.
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.
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 }
If F creates colimits and F ≅ G, then G creates colimits.
Equations
- CategoryTheory.createsColimitsOfNatIso h = { CreatesColimitsOfShape := fun {J : Type ?u.68} [CategoryTheory.Category.{?u.67, ?u.68} J] => CategoryTheory.createsColimitsOfShapeOfNatIso h }
If F creates colimits of shape J and J ≌ J', then F creates colimits of shape J'.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
Any cone lifts through the identity functor.
Equations
- One or more equations did not get rendered due to their size.
The identity functor creates all limits.
Equations
- One or more equations did not get rendered due to their size.
Any cocone lifts through the identity functor.
Equations
- One or more equations did not get rendered due to their size.
The identity functor creates all colimits.
Equations
- One or more equations did not get rendered due to their size.
Satisfy the inhabited linter
Equations
- CategoryTheory.inhabitedLiftableCone c = { default := CategoryTheory.idLiftsCone c }
Equations
- CategoryTheory.inhabitedLiftableCocone c = { default := CategoryTheory.idLiftsCocone c }
Satisfy the inhabited linter
Equations
- CategoryTheory.inhabitedLiftsToLimit K F c t = { default := CategoryTheory.liftsToLimitOfCreates K F c t }
Equations
- CategoryTheory.inhabitedLiftsToColimit K F c t = { default := CategoryTheory.liftsToColimitOfCreates K F c t }
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.compCreatesLimitsOfShape F G = { CreatesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
Equations
- CategoryTheory.compCreatesLimits F G = { CreatesLimitsOfShape := fun {J : Type ?u.90} [CategoryTheory.Category.{?u.89, ?u.90} J] => inferInstance }
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.compCreatesColimitsOfShape F G = { CreatesColimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
Equations
- CategoryTheory.compCreatesColimits F G = { CreatesColimitsOfShape := fun {J : Type ?u.90} [CategoryTheory.Category.{?u.89, ?u.90} J] => inferInstance }