# 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".

class CategoryTheory.Limits.PreservesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) w)

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
class CategoryTheory.Limits.PreservesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) w)

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
class CategoryTheory.Limits.PreservesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

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 :
Instances
class CategoryTheory.Limits.PreservesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

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 :
Instances
class CategoryTheory.Limits.PreservesLimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

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].

• preservesLimitsOfShape : {J : Type w} →
Instances
@[reducible, inline]
abbrev CategoryTheory.Limits.PreservesLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

We say that F preserves (small) limits if it sends small limit cones over any diagram to limit cones.

Equations
Instances For
class CategoryTheory.Limits.PreservesColimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

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].

• preservesColimitsOfShape : {J : Type w} →
Instances
@[reducible, inline]
abbrev CategoryTheory.Limits.PreservesColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

We say that F preserves (small) limits if it sends small limit cones over any diagram to limit cones.

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

A convenience function for PreservesLimit, which takes the functor as an explicit argument to guide typeclass resolution.

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

A convenience function for PreservesColimit, which takes the functor as an explicit argument to guide typeclass resolution.

Equations
Instances For
instance CategoryTheory.Limits.preservesLimit_subsingleton {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Equations
• =
instance CategoryTheory.Limits.preservesColimit_subsingleton {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Equations
• =
instance CategoryTheory.Limits.preservesLimitsOfShape_subsingleton {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Equations
• =
instance CategoryTheory.Limits.preservesColimitsOfShape_subsingleton {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Equations
• =
instance CategoryTheory.Limits.preserves_limits_subsingleton {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
• =
instance CategoryTheory.Limits.preserves_colimits_subsingleton {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
• =
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.instHasLimitCompOfPreservesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :
Equations
• =
instance CategoryTheory.Limits.instHasColimitCompOfPreservesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } :
Equations
• =
instance CategoryTheory.Limits.compPreservesLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.PreservesLimit (K.comp F) G] :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.compPreservesLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
Equations
• = { preservesLimit := fun {K : } => inferInstance }
instance CategoryTheory.Limits.compPreservesLimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
Equations
• = { preservesLimitsOfShape := fun {J : Type w} [] => inferInstance }
instance CategoryTheory.Limits.compPreservesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.PreservesColimit (K.comp F) G] :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.compPreservesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
Equations
• = { preservesColimit := fun {K : } => inferInstance }
instance CategoryTheory.Limits.compPreservesColimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
Equations
• = { preservesColimitsOfShape := fun {J : Type w} [] => inferInstance }
def CategoryTheory.Limits.preservesLimitOfPreservesLimitCone {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {t : } (hF : CategoryTheory.Limits.IsLimit (F.mapCone t)) :

If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) {F : } {G : } (h : F G) :

Transfer preservation of a limit along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

Transfer preservation of limits of shape along a natural isomorphism in the functor.

Equations
• = { preservesLimit := fun {K : } => }
Instances For
def CategoryTheory.Limits.preservesLimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

Transfer preservation of limits along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {J' : Type w₂} [] (e : J J') (F : ) :

Transfer preservation of limits along an equivalence in the shape.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

A functor preserving larger limits also preserves smaller limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitsOfSizeShrink {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

PreservesLimitsOfSizeShrink.{w w'} F tries to obtain PreservesLimitsOfSize.{w w'} F from some other PreservesLimitsOfSize F.

Equations
Instances For

Preserving limits at any universe level implies preserving limits in universe 0.

Equations
Instances For
def CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {F : } {t : } (hF : CategoryTheory.Limits.IsColimit (F.mapCocone t)) :

If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) :

Transfer preservation of colimits along a natural isomorphism in the shape.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) {F : } {G : } (h : F G) :

Transfer preservation of a colimit along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

Transfer preservation of colimits of shape along a natural isomorphism in the functor.

Equations
• = { preservesColimit := fun {K : } => }
Instances For
def CategoryTheory.Limits.preservesColimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

Transfer preservation of colimits along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {J' : Type w₂} [] (e : J J') (F : ) :

Transfer preservation of colimits along an equivalence in the shape.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

A functor preserving larger colimits also preserves smaller colimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitsOfSizeShrink {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

PreservesColimitsOfSizeShrink.{w w'} F tries to obtain PreservesColimitsOfSize.{w w'} F from some other PreservesColimitsOfSize F.

Equations
Instances For

Preserving colimits at any universe implies preserving colimits at universe 0.

Equations
Instances For
class CategoryTheory.Limits.ReflectsLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) w)

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
class CategoryTheory.Limits.ReflectsColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) w)

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
class CategoryTheory.Limits.ReflectsLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

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 :
Instances
class CategoryTheory.Limits.ReflectsColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

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 :
Instances
class CategoryTheory.Limits.ReflectsLimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

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.

• reflectsLimitsOfShape : {J : Type w} →
Instances
@[reducible, inline]
abbrev CategoryTheory.Limits.ReflectsLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

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
class CategoryTheory.Limits.ReflectsColimitsOfSize {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

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.

• reflectsColimitsOfShape : {J : Type w} →
Instances
@[reducible, inline]
abbrev CategoryTheory.Limits.ReflectsColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

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
def CategoryTheory.Limits.isLimitOfReflects {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } (F : ) {c : } (t : CategoryTheory.Limits.IsLimit (F.mapCone c)) :

A convenience function for ReflectsLimit, which takes the functor as an explicit argument to guide typeclass resolution.

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

A convenience function for ReflectsColimit, which takes the functor as an explicit argument to guide typeclass resolution.

Equations
Instances For
instance CategoryTheory.Limits.reflectsLimit_subsingleton {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Equations
• =
instance CategoryTheory.Limits.reflectsColimit_subsingleton {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Equations
• =
instance CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Equations
• =
instance CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :
Equations
• =
instance CategoryTheory.Limits.reflects_limits_subsingleton {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
• =
instance CategoryTheory.Limits.reflects_colimits_subsingleton {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
• =
@[instance 100]
instance CategoryTheory.Limits.reflectsLimitOfReflectsLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Equations
• = CategoryTheory.Limits.ReflectsLimitsOfShape.reflectsLimit
@[instance 100]
instance CategoryTheory.Limits.reflectsColimitOfReflectsColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :
Equations
• = CategoryTheory.Limits.ReflectsColimitsOfShape.reflectsColimit
@[instance 100]
instance CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsLimits {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) [] :
Equations
• = CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsLimitsOfShape
@[instance 100]
instance CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsColimits {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) [] :
Equations
• = CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsColimitsOfShape
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.compReflectsLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.ReflectsLimit (K.comp F) G] :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.compReflectsLimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
Equations
• = { reflectsLimit := fun {K : } => inferInstance }
instance CategoryTheory.Limits.compReflectsLimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
Equations
• = { reflectsLimitsOfShape := fun {J : Type w} [] => inferInstance }
instance CategoryTheory.Limits.compReflectsColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.ReflectsColimit (K.comp F) G] :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.compReflectsColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) :
Equations
• = { reflectsColimit := fun {K : } => inferInstance }
instance CategoryTheory.Limits.compReflectsColimits {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :
Equations
• = { reflectsColimitsOfShape := fun {J : Type w} [] => inferInstance }
def CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.PreservesLimit K (F.comp G)] [CategoryTheory.Limits.ReflectsLimit (K.comp F) G] :

If F ⋙ G preserves limits for K, and G reflects limits for K ⋙ F, then F preserves limits for K.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp G)] :

If F ⋙ G preserves limits of shape J and G reflects limits of shape J, then F preserves limits of shape J.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :

If F ⋙ G preserves limits and G reflects limits, then F preserves limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) {F : } {G : } (h : F G) :

Transfer reflection of a limit along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

Transfer reflection of limits of shape along a natural isomorphism in the functor.

Equations
• = { reflectsLimit := fun {K : } => }
Instances For
def CategoryTheory.Limits.reflectsLimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

Transfer reflection of limits along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {J' : Type w₂} [] (e : J J') (F : ) :

Transfer reflection of limits along an equivalence in the shape.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

A functor reflecting larger limits also reflects smaller limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitsOfSizeShrink {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

reflectsLimitsOfSizeShrink.{w w'} F tries to obtain reflectsLimitsOfSize.{w w'} F from some other reflectsLimitsOfSize F.

Equations
Instances For
def CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

Reflecting limits at any universe implies reflecting limits at universe 0.

Equations
Instances For
def CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) (G : ) [G.ReflectsIsomorphisms] :

If the limit of F exists and G preserves it, then if G reflects isomorphisms then it reflects the limit of F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {G : } [G.ReflectsIsomorphisms] :

If C has limits of shape J and G preserves them, then if G reflects isomorphisms then it reflects limits of shape J.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {G : } [G.ReflectsIsomorphisms] [] [] :

If C has limits and G preserves limits, then if G reflects isomorphisms then it reflects limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K : } {E : Type u₃} [ℰ : ] (F : ) (G : ) [CategoryTheory.Limits.PreservesColimit K (F.comp G)] [CategoryTheory.Limits.ReflectsColimit (K.comp F) G] :

If F ⋙ G preserves colimits for K, and G reflects colimits for K ⋙ F, then F preserves colimits for K.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {E : Type u₃} [ℰ : ] (F : ) (G : ) [] :

If F ⋙ G preserves colimits of shape J and G reflects colimits of shape J, then F preserves colimits of shape J.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [ℰ : ] (F : ) (G : ) [] [] :

If F ⋙ G preserves colimits and G reflects colimits, then F preserves colimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitOfIsoDiagram {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {K₁ : } {K₂ : } (F : ) (h : K₁ K₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) {F : } {G : } (h : F G) :

Transfer reflection of a colimit along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {F : } {G : } (h : F G) :

Transfer reflection of colimits of shape along a natural isomorphism in the functor.

Equations
• = { reflectsColimit := fun {K : } => }
Instances For
def CategoryTheory.Limits.reflectsColimitsOfNatIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (h : F G) [] :

Transfer reflection of colimits along a natural isomorphism in the functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {J' : Type w₂} [] (e : J J') (F : ) :

Transfer reflection of colimits along an equivalence in the shape.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

A functor reflecting larger colimits also reflects smaller colimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitsOfSizeShrink {C : Type u₁} [] {D : Type u₂} [] (F : ) [] :

reflectsColimitsOfSizeShrink.{w w'} F tries to obtain reflectsColimitsOfSize.{w w'} F from some other reflectsColimitsOfSize F.

Equations
Instances For

Reflecting colimits at any universe implies reflecting colimits at universe 0.

Equations
Instances For
def CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (F : ) (G : ) [G.ReflectsIsomorphisms] :

If the colimit of F exists and G preserves it, then if G reflects isomorphisms then it reflects the colimit of F.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {J : Type w} {G : } [G.ReflectsIsomorphisms] :

If C has colimits of shape J and G preserves them, then if G reflects isomorphisms then it reflects colimits of shape J.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {G : } [G.ReflectsIsomorphisms] [] [] :

If C has colimits and G preserves colimits, then if G reflects isomorphisms then it reflects colimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Limits.fullyFaithfulReflectsLimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.Full] [F.Faithful] :

A fully faithful functor reflects limits.

Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Limits.fullyFaithfulReflectsColimits {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.Full] [F.Faithful] :

A fully faithful functor reflects colimits.

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