Preservation and reflection of (co)limits. #
There are various distinct notions of "preserving limits". The one we aim to capture here is: A functor F : C ⥤ D "preserves limits" if it sends every limit cone in C to a limit cone in D. Informally, F preserves all the limits which exist in C.
Note that:
Of course, we do not want to require F to strictly take chosen limit cones of C to chosen limit cones of D. Indeed, the above definition makes no reference to a choice of limit cones so it makes sense without any conditions on C or D.
Some diagrams in C may have no limit. In this case, there is no condition on the behavior of F on such diagrams. There are other notions (such as "flat functor") which impose conditions also on diagrams in C with no limits, but these are not considered here.
In order to be able to express the property of preserving limits of a certain form, we say that a functor F preserves the limit of a diagram K if F sends every limit cone on K to a limit cone. This is vacuously satisfied when K does not admit a limit, which is consistent with the above definition of "preserves limits".
A functor F preserves limits of K (written as PreservesLimit K F)
if F maps any limit cone over K to a limit cone.
Instances
A functor F preserves colimits of K (written as PreservesColimit K F)
if F maps any colimit cocone over K to a colimit cocone.
Instances
We say that F preserves limits of shape J if F preserves limits for every diagram
K : J ⥤ C, i.e., F maps limit cones over K to limit cones.
- preservesLimit {K : Functor J C} : PreservesLimit K F
Instances
We say that F preserves colimits of shape J if F preserves colimits for every diagram
K : J ⥤ C, i.e., F maps colimit cocones over K to colimit cocones.
- preservesColimit {K : Functor J C} : PreservesColimit K F
Instances
PreservesLimitsOfSize.{v u} F means that F sends all limit cones over any
diagram J ⥤ C to limit cones, where J : Type u with [Category.{v} J].
Instances
We say that F preserves (small) limits if it sends small
limit cones over any diagram to limit cones.
Equations
Instances For
PreservesColimitsOfSize.{v u} F means that F sends all colimit cocones over any
diagram J ⥤ C to colimit cocones, where J : Type u with [Category.{v} J].
Instances
We say that F preserves (small) limits if it sends small
limit cones over any diagram to limit cones.
Equations
Instances For
A convenience function for PreservesLimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
Instances For
A convenience function for PreservesColimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
Instances For
If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.
Transfer preservation of limits along a natural isomorphism in the diagram.
Transfer preservation of a limit along a natural isomorphism in the functor.
Transfer preservation of limits of shape along a natural isomorphism in the functor.
Transfer preservation of limits along a natural isomorphism in the functor.
Transfer preservation of limits along an equivalence in the shape.
A functor preserving larger limits also preserves smaller limits.
PreservesLimitsOfSize_shrink.{w w'} F tries to obtain PreservesLimitsOfSize.{w w'} F
from some other PreservesLimitsOfSize F.
Preserving limits at any universe level implies preserving limits in universe 0.
If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.
Transfer preservation of colimits along a natural isomorphism in the shape.
Transfer preservation of a colimit along a natural isomorphism in the functor.
Transfer preservation of colimits of shape along a natural isomorphism in the functor.
Transfer preservation of colimits along a natural isomorphism in the functor.
Transfer preservation of colimits along an equivalence in the shape.
A functor preserving larger colimits also preserves smaller colimits.
PreservesColimitsOfSize_shrink.{w w'} F tries to obtain PreservesColimitsOfSize.{w w'} F
from some other PreservesColimitsOfSize F.
Preserving colimits at any universe implies preserving colimits at universe 0.
A functor F : C ⥤ D reflects limits for K : J ⥤ C if
whenever the image of a cone over K under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
Instances
A functor F : C ⥤ D reflects colimits for K : J ⥤ C if
whenever the image of a cocone over K under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
Instances
A functor F : C ⥤ D reflects limits of shape J if
whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
- reflectsLimit {K : Functor J C} : ReflectsLimit K F
Instances
A functor F : C ⥤ D reflects colimits of shape J if
whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
- reflectsColimit {K : Functor J C} : ReflectsColimit K F
Instances
A functor F : C ⥤ D reflects limits if
whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
Instances
A functor F : C ⥤ D reflects (small) limits if
whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
Equations
Instances For
A functor F : C ⥤ D reflects colimits if
whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
Instances
A functor F : C ⥤ D reflects (small) colimits if
whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
Equations
Instances For
A convenience function for ReflectsLimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
Instances For
A convenience function for ReflectsColimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
Instances For
If F ⋙ G preserves limits for K, and G reflects limits for K ⋙ F,
then F preserves limits for K.
If F ⋙ G preserves limits of shape J and G reflects limits of shape J, then F preserves
limits of shape J.
If F ⋙ G preserves limits and G reflects limits, then F preserves limits.
Transfer reflection of limits along a natural isomorphism in the diagram.
Transfer reflection of a limit along a natural isomorphism in the functor.
Transfer reflection of limits of shape along a natural isomorphism in the functor.
Transfer reflection of limits along a natural isomorphism in the functor.
Transfer reflection of limits along an equivalence in the shape.
A functor reflecting larger limits also reflects smaller limits.
reflectsLimitsOfSize_shrink.{w w'} F tries to obtain reflectsLimitsOfSize.{w w'} F
from some other reflectsLimitsOfSize F.
Reflecting limits at any universe implies reflecting limits at universe 0.
If the limit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the limit of F.
If C has limits of shape J and G preserves them, then if G reflects isomorphisms then it
reflects limits of shape J.
If C has limits and G preserves limits, then if G reflects isomorphisms then it reflects
limits.
If F ⋙ G preserves colimits for K, and G reflects colimits for K ⋙ F,
then F preserves colimits for K.
If F ⋙ G preserves colimits of shape J and G reflects colimits of shape J, then F
preserves colimits of shape J.
If F ⋙ G preserves colimits and G reflects colimits, then F preserves colimits.
Transfer reflection of colimits along a natural isomorphism in the diagram.
Transfer reflection of a colimit along a natural isomorphism in the functor.
Transfer reflection of colimits of shape along a natural isomorphism in the functor.
Transfer reflection of colimits along a natural isomorphism in the functor.
Transfer reflection of colimits along an equivalence in the shape.
A functor reflecting larger colimits also reflects smaller colimits.
reflectsColimitsOfSize_shrink.{w w'} F tries to obtain reflectsColimitsOfSize.{w w'} F
from some other reflectsColimitsOfSize F.
Reflecting colimits at any universe implies reflecting colimits at universe 0.
If the colimit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the colimit of F.
If C has colimits of shape J and G preserves them, then if G reflects isomorphisms then it
reflects colimits of shape J.
If C has colimits and G preserves colimits, then if G reflects isomorphisms then it reflects
colimits.
A fully faithful functor reflects limits.
A fully faithful functor reflects colimits.