mathlib documentation

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:

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] :
J CC DType (max u₁ u₂ v)

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
@[class]
structure category_theory.limits.preserves_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] :
J CC DType (max u₁ u₂ v)

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
@[class]
structure category_theory.limits.preserves_limits_of_shape {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type v) [category_theory.small_category J] :
C DType (max u₁ u₂ v)

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
@[class]
structure category_theory.limits.preserves_colimits_of_shape {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type v) [category_theory.small_category J] :
C DType (max u₁ u₂ v)

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
@[class]
structure category_theory.limits.preserves_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
C DType (max u₁ u₂ (v+1))

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

Instances

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

Equations

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

Equations
@[class]
structure category_theory.limits.reflects_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] :
J CC DType (max u₁ u₂ v)

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]
structure category_theory.limits.reflects_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type v} [category_theory.small_category J] :
J CC DType (max u₁ u₂ v)

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]
structure category_theory.limits.reflects_limits_of_shape {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type v) [category_theory.small_category J] :
C DType (max u₁ u₂ v)

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
@[class]
structure category_theory.limits.reflects_colimits_of_shape {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type v) [category_theory.small_category J] :
C DType (max u₁ u₂ v)

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
@[class]
structure category_theory.limits.reflects_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
C DType (max u₁ u₂ (v+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.

Instances
@[class]
structure category_theory.limits.reflects_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
C DType (max u₁ u₂ (v+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.

Instances