mathlib3 documentation

category_theory.limits.preserves.basic

Preservation and reflection of (co)limits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 w} [category_theory.category J] (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)

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

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C D) :
Type (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.

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C D) :
Type (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.

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

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
@[reducible]
def category_theory.limits.preserves_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))

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
@[reducible]
def category_theory.limits.preserves_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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.

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

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C D) :
Type (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.

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Type (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.

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

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.reflects_colimits_of_size
@[reducible]
def category_theory.limits.reflects_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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.

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

Equations

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

Equations