# mathlibdocumentation

category_theory.limits.preserves.basic

# 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]
structure category_theory.limits.preserves_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• preserves :

A functor F preserves limits of K (written as preserves_limit K F) if F maps any limit cone over K to a limit cone.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_limit
@[class]
structure category_theory.limits.preserves_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• preserves :

A functor F preserves colimits of K (written as preserves_colimit K F) if F maps any colimit cocone over K to a colimit cocone.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_colimit
@[class]
structure category_theory.limits.preserves_limits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• preserves_limit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_limits_of_shape
@[class]
structure category_theory.limits.preserves_colimits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• preserves_colimit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_colimits_of_shape
@[nolint, class]
structure category_theory.limits.preserves_limits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• preserves_limits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

preserves_limits_of_size.{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 of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_limits_of_size
def category_theory.limits.preserves_limits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

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

@[nolint, class]
structure category_theory.limits.preserves_colimits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• preserves_colimits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

preserves_colimits_of_size.{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 of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_colimits_of_size
def category_theory.limits.preserves_colimits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

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

def category_theory.limits.is_limit_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D)  :

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

Equations
def category_theory.limits.is_colimit_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D)  :

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

Equations
@[protected, instance]
def category_theory.limits.preserves_limit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_colimit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_limits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_colimits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_limits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_colimits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_limits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_colimits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
def category_theory.limits.preserves_limit_of_preserves_limit_cone {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (hF : category_theory.limits.is_limit (F.map_cone t)) :

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

Equations
def category_theory.limits.preserves_limit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

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

Equations
def category_theory.limits.preserves_limit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.preserves_limits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.preserves_limits_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.preserves_limits_of_shape_of_equiv {C : Type u₁} {D : Type u₂} {J : Type w} {J' : Type w₂} (e : J J') (F : C D)  :

Transfer preservation of limits along a equivalence in the shape.

Equations
def category_theory.limits.preserves_colimit_of_preserves_colimit_cocone {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {F : C D} (hF : category_theory.limits.is_colimit (F.map_cocone t)) :

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

Equations
def category_theory.limits.preserves_colimit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

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

Equations
def category_theory.limits.preserves_colimit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.preserves_colimits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.preserves_colimits_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.preserves_colimits_of_shape_of_equiv {C : Type u₁} {D : Type u₂} {J : Type w} {J' : Type w₂} (e : J J') (F : C D)  :

Transfer preservation of colimits along a equivalence in the shape.

Equations
@[class]
structure category_theory.limits.reflects_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• reflects :

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 of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_limit
@[class]
structure category_theory.limits.reflects_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• reflects :

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 of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_colimit
@[class]
structure category_theory.limits.reflects_limits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• reflects_limit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_limits_of_shape
@[class]
structure category_theory.limits.reflects_colimits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• reflects_colimit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_colimits_of_shape
@[nolint, class]
structure category_theory.limits.reflects_limits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• reflects_limits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

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 of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_limits_of_size
def category_theory.limits.reflects_limits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ 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.

@[nolint, class]
structure category_theory.limits.reflects_colimits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• reflects_colimits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

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 of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_colimits_of_size
def category_theory.limits.reflects_colimits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ 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.

def category_theory.limits.is_limit_of_reflects {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D) (t : category_theory.limits.is_limit (F.map_cone c))  :

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

Equations
def category_theory.limits.is_colimit_of_reflects {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D) (t : category_theory.limits.is_colimit (F.map_cocone c))  :

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

Equations
@[protected, instance]
def category_theory.limits.reflects_limit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_colimit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_limits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_colimits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_limits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_colimits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_limit_of_reflects_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :
Equations
@[protected, instance]
def category_theory.limits.reflects_colimit_of_reflects_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :
Equations
@[protected, instance]
def category_theory.limits.reflects_limits_of_shape_of_reflects_limits {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D)  :
Equations
@[protected, instance]
def category_theory.limits.reflects_colimits_of_shape_of_reflects_colimits {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_limits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_colimits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
def category_theory.limits.preserves_limit_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ (F G)] [ G] :

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

Equations
def category_theory.limits.preserves_limits_of_shape_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

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

Equations
def category_theory.limits.preserves_limits_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

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

Equations
def category_theory.limits.reflects_limit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

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

Equations
def category_theory.limits.reflects_limit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.reflects_limits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.reflects_limits_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

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

Equations
noncomputable def category_theory.limits.reflects_limit_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} (F : J C) (G : C D)  :

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

Equations
noncomputable def category_theory.limits.reflects_limits_of_shape_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} {G : C D}  :

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

Equations
noncomputable def category_theory.limits.reflects_limits_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {G : C D}  :

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

Equations
def category_theory.limits.preserves_colimit_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :

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

Equations
def category_theory.limits.preserves_colimits_of_shape_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

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

Equations
def category_theory.limits.preserves_colimits_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

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

Equations
def category_theory.limits.reflects_colimit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

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

Equations
def category_theory.limits.reflects_colimit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.reflects_colimits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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

Equations
def category_theory.limits.reflects_colimits_of_nat_iso {C : Type u₁} {D : Type u₂} {F G : C D} (h : F G)  :

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

Equations
noncomputable def category_theory.limits.reflects_colimit_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} (F : J C) (G : C D)  :

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

Equations
noncomputable def category_theory.limits.reflects_colimits_of_shape_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} {G : C D}  :

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

Equations
noncomputable def category_theory.limits.reflects_colimits_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {G : C D}  :

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

Equations
def category_theory.limits.fully_faithful_reflects_limits {C : Type u₁} {D : Type u₂} (F : C D)  :

A fully faithful functor reflects limits.

Equations
def category_theory.limits.fully_faithful_reflects_colimits {C : Type u₁} {D : Type u₂} (F : C D)  :

A fully faithful functor reflects colimits.

Equations