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

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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.

source
@[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
source
@[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.

source
def category_theory.limits.is_limit_of_preserves {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) {c : category_theory.limits.cone K} (t : category_theory.limits.is_limit c) [category_theory.limits.preserves_limit K F] :
category_theory.limits.is_limit (F.map_cone c)

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

Equations
source
def category_theory.limits.is_colimit_of_preserves {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) {c : category_theory.limits.cocone K} (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit K F] :
category_theory.limits.is_colimit (F.map_cocone c)

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

Equations
source
@[protected, instance]
def category_theory.limits.preserves_limit_subsingleton {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) :
subsingleton (category_theory.limits.preserves_limit K F)
source
@[protected, instance]
def category_theory.limits.preserves_colimit_subsingleton {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) :
subsingleton (category_theory.limits.preserves_colimit K F)
source
@[protected, instance]
def category_theory.limits.preserves_limits_of_shape_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) :
subsingleton (category_theory.limits.preserves_limits_of_shape J F)
source
@[protected, instance]
def category_theory.limits.preserves_colimits_of_shape_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) :
subsingleton (category_theory.limits.preserves_colimits_of_shape J F)
source
@[protected, instance]
def category_theory.limits.preserves_limits_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
subsingleton (category_theory.limits.preserves_limits_of_size F)
source
@[protected, instance]
def category_theory.limits.preserves_colimits_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
subsingleton (category_theory.limits.preserves_colimits_of_size F)
source
@[protected, instance]
def category_theory.limits.id_preserves_limits {C : Type u₁} [category_theory.category C] :
category_theory.limits.preserves_limits_of_size (𝟭 C)
Equations
source
@[protected, instance]
def category_theory.limits.id_preserves_colimits {C : Type u₁} [category_theory.category C] :
category_theory.limits.preserves_colimits_of_size (𝟭 C)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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} {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_limit K F] [category_theory.limits.preserves_limit (K ⋙ F) G] :
category_theory.limits.preserves_limit K (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_limits_of_shape J F] [category_theory.limits.preserves_limits_of_shape J G] :
category_theory.limits.preserves_limits_of_shape J (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_preserves_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_limits_of_size F] [category_theory.limits.preserves_limits_of_size G] :
category_theory.limits.preserves_limits_of_size (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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} {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_colimit K F] [category_theory.limits.preserves_colimit (K ⋙ F) G] :
category_theory.limits.preserves_colimit K (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_colimits_of_shape J F] [category_theory.limits.preserves_colimits_of_shape J G] :
category_theory.limits.preserves_colimits_of_shape J (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_preserves_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_colimits_of_size F] [category_theory.limits.preserves_colimits_of_size G] :
category_theory.limits.preserves_colimits_of_size (F ⋙ G)
Equations
source
def category_theory.limits.preserves_limit_of_preserves_limit_cone {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} {t : category_theory.limits.cone K} (h : category_theory.limits.is_limit t) (hF : category_theory.limits.is_limit (F.map_cone t)) :
category_theory.limits.preserves_limit K F

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

Equations
source
def category_theory.limits.preserves_limit_of_iso_diagram {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [category_theory.limits.preserves_limit K₁ F] :
category_theory.limits.preserves_limit K₂ F

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

Equations
source
def category_theory.limits.preserves_limit_of_nat_iso {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 G : C ⥤ D} (h : F ≅ G) [category_theory.limits.preserves_limit K F] :
category_theory.limits.preserves_limit K G

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

Equations
source
def category_theory.limits.preserves_limits_of_shape_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.preserves_limits_of_shape J F] :
category_theory.limits.preserves_limits_of_shape J G

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

Equations
source
def category_theory.limits.preserves_limits_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.preserves_limits_of_size F] :
category_theory.limits.preserves_limits_of_size G

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

Equations
source
def category_theory.limits.preserves_limits_of_shape_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {J' : Type w₂} [category_theory.category J'] (e : J ≌ J') (F : C ⥤ D) [category_theory.limits.preserves_limits_of_shape J F] :
category_theory.limits.preserves_limits_of_shape J' F

Transfer preservation of limits along a equivalence in the shape.

Equations
source
def category_theory.limits.preserves_limits_of_size_shrink {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits_of_size F] :
category_theory.limits.preserves_limits_of_size F

preserves_limits_of_size_shrink.{w w'} F tries to obtain preserves_limits_of_size.{w w'} F from some other preserves_limits_of_size F.

Equations
source
def category_theory.limits.preserves_smallest_limits_of_preserves_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits_of_size F] :
category_theory.limits.preserves_limits_of_size F

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

Equations
source
def category_theory.limits.preserves_colimit_of_preserves_colimit_cocone {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} {t : category_theory.limits.cocone K} (h : category_theory.limits.is_colimit t) (hF : category_theory.limits.is_colimit (F.map_cocone t)) :
category_theory.limits.preserves_colimit K F

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

Equations
source
def category_theory.limits.preserves_colimit_of_iso_diagram {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [category_theory.limits.preserves_colimit K₁ F] :
category_theory.limits.preserves_colimit K₂ F

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

Equations
source
def category_theory.limits.preserves_colimit_of_nat_iso {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 G : C ⥤ D} (h : F ≅ G) [category_theory.limits.preserves_colimit K F] :
category_theory.limits.preserves_colimit K G

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

Equations
source
def category_theory.limits.preserves_colimits_of_shape_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.preserves_colimits_of_shape J F] :
category_theory.limits.preserves_colimits_of_shape J G

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

Equations
source
def category_theory.limits.preserves_colimits_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.preserves_colimits_of_size F] :
category_theory.limits.preserves_colimits_of_size G

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

Equations
source
def category_theory.limits.preserves_colimits_of_shape_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {J' : Type w₂} [category_theory.category J'] (e : J ≌ J') (F : C ⥤ D) [category_theory.limits.preserves_colimits_of_shape J F] :
category_theory.limits.preserves_colimits_of_shape J' F

Transfer preservation of colimits along a equivalence in the shape.

Equations
source
def category_theory.limits.preserves_colimits_of_size_shrink {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_colimits_of_size F] :
category_theory.limits.preserves_colimits_of_size F

preserves_colimits_of_size_shrink.{w w'} F tries to obtain preserves_colimits_of_size.{w w'} F from some other preserves_colimits_of_size F.

Equations
source
def category_theory.limits.preserves_smallest_colimits_of_preserves_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_colimits_of_size F] :
category_theory.limits.preserves_colimits_of_size F

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

Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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.

source
@[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
source
@[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.

source
def category_theory.limits.is_limit_of_reflects {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) {c : category_theory.limits.cone K} (t : category_theory.limits.is_limit (F.map_cone c)) [category_theory.limits.reflects_limit K F] :
category_theory.limits.is_limit c

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

Equations
source
def category_theory.limits.is_colimit_of_reflects {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) {c : category_theory.limits.cocone K} (t : category_theory.limits.is_colimit (F.map_cocone c)) [category_theory.limits.reflects_colimit K F] :
category_theory.limits.is_colimit c

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

Equations
source
@[protected, instance]
def category_theory.limits.reflects_limit_subsingleton {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) :
subsingleton (category_theory.limits.reflects_limit K F)
source
@[protected, instance]
def category_theory.limits.reflects_colimit_subsingleton {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) :
subsingleton (category_theory.limits.reflects_colimit K F)
source
@[protected, instance]
def category_theory.limits.reflects_limits_of_shape_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) :
subsingleton (category_theory.limits.reflects_limits_of_shape J F)
source
@[protected, instance]
def category_theory.limits.reflects_colimits_of_shape_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) :
subsingleton (category_theory.limits.reflects_colimits_of_shape J F)
source
@[protected, instance]
def category_theory.limits.reflects_limits_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
subsingleton (category_theory.limits.reflects_limits_of_size F)
source
@[protected, instance]
def category_theory.limits.reflects_colimits_subsingleton {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
subsingleton (category_theory.limits.reflects_colimits_of_size F)
source
@[protected, instance]
def category_theory.limits.reflects_limit_of_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] (K : J ⥤ C) (F : C ⥤ D) [H : category_theory.limits.reflects_limits_of_shape J F] :
category_theory.limits.reflects_limit K F
Equations
source
@[protected, instance]
def category_theory.limits.reflects_colimit_of_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] (K : J ⥤ C) (F : C ⥤ D) [H : category_theory.limits.reflects_colimits_of_shape J F] :
category_theory.limits.reflects_colimit K F
Equations
source
@[protected, instance]
def category_theory.limits.reflects_limits_of_shape_of_reflects_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) [H : category_theory.limits.reflects_limits_of_size F] :
category_theory.limits.reflects_limits_of_shape J F
Equations
source
@[protected, instance]
def category_theory.limits.reflects_colimits_of_shape_of_reflects_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (J : Type w) [category_theory.category J] (F : C ⥤ D) [H : category_theory.limits.reflects_colimits_of_size F] :
category_theory.limits.reflects_colimits_of_shape J F
Equations
source
@[protected, instance]
def category_theory.limits.id_reflects_limits {C : Type u₁} [category_theory.category C] :
category_theory.limits.reflects_limits_of_size (𝟭 C)
Equations
source
@[protected, instance]
def category_theory.limits.id_reflects_colimits {C : Type u₁} [category_theory.category C] :
category_theory.limits.reflects_colimits_of_size (𝟭 C)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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} {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.reflects_limit K F] [category_theory.limits.reflects_limit (K ⋙ F) G] :
category_theory.limits.reflects_limit K (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.reflects_limits_of_shape J F] [category_theory.limits.reflects_limits_of_shape J G] :
category_theory.limits.reflects_limits_of_shape J (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_reflects_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.reflects_limits_of_size F] [category_theory.limits.reflects_limits_of_size G] :
category_theory.limits.reflects_limits_of_size (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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} {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.reflects_colimit K F] [category_theory.limits.reflects_colimit (K ⋙ F) G] :
category_theory.limits.reflects_colimit K (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_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] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.reflects_colimits_of_shape J F] [category_theory.limits.reflects_colimits_of_shape J G] :
category_theory.limits.reflects_colimits_of_shape J (F ⋙ G)
Equations
source
@[protected, instance]
def category_theory.limits.comp_reflects_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.reflects_colimits_of_size F] [category_theory.limits.reflects_colimits_of_size G] :
category_theory.limits.reflects_colimits_of_size (F ⋙ G)
Equations
source
def category_theory.limits.preserves_limit_of_reflects_of_preserves {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {K : J ⥤ C} {E : Type u₃} [ℰ : category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) [category_theory.limits.preserves_limit K (F ⋙ G)] [category_theory.limits.reflects_limit (K ⋙ F) G] :
category_theory.limits.preserves_limit K F

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

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

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

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

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

Equations
source
def category_theory.limits.reflects_limit_of_iso_diagram {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [category_theory.limits.reflects_limit K₁ F] :
category_theory.limits.reflects_limit K₂ F

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

Equations
source
def category_theory.limits.reflects_limit_of_nat_iso {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 G : C ⥤ D} (h : F ≅ G) [category_theory.limits.reflects_limit K F] :
category_theory.limits.reflects_limit K G

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

Equations
source
def category_theory.limits.reflects_limits_of_shape_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.reflects_limits_of_shape J F] :
category_theory.limits.reflects_limits_of_shape J G

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

Equations
source
def category_theory.limits.reflects_limits_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.reflects_limits_of_size F] :
category_theory.limits.reflects_limits_of_size G

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

Equations
source
def category_theory.limits.reflects_limits_of_shape_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {J' : Type w₂} [category_theory.category J'] (e : J ≌ J') (F : C ⥤ D) [category_theory.limits.reflects_limits_of_shape J F] :
category_theory.limits.reflects_limits_of_shape J' F

Transfer reflection of limits along a equivalence in the shape.

Equations
source
def category_theory.limits.reflects_limits_of_size_shrink {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.reflects_limits_of_size F] :
category_theory.limits.reflects_limits_of_size F

reflects_limits_of_size_shrink.{w w'} F tries to obtain reflects_limits_of_size.{w w'} F from some other reflects_limits_of_size F.

Equations
source
def category_theory.limits.reflects_smallest_limits_of_reflects_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.reflects_limits_of_size F] :
category_theory.limits.reflects_limits_of_size F

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

Equations
source
noncomputable def category_theory.limits.reflects_limit_of_reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (F : J ⥤ C) (G : C ⥤ D) [category_theory.reflects_isomorphisms G] [category_theory.limits.has_limit F] [category_theory.limits.preserves_limit F G] :
category_theory.limits.reflects_limit F G

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

Equations
source
noncomputable def category_theory.limits.reflects_limits_of_shape_of_reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {G : C ⥤ D} [category_theory.reflects_isomorphisms G] [category_theory.limits.has_limits_of_shape J C] [category_theory.limits.preserves_limits_of_shape J G] :
category_theory.limits.reflects_limits_of_shape J G

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

Equations
source
noncomputable def category_theory.limits.reflects_limits_of_reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : C ⥤ D} [category_theory.reflects_isomorphisms G] [category_theory.limits.has_limits_of_size C] [category_theory.limits.preserves_limits_of_size G] :
category_theory.limits.reflects_limits_of_size G

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

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

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

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

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

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

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

Equations
source
def category_theory.limits.reflects_colimit_of_iso_diagram {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [category_theory.limits.reflects_colimit K₁ F] :
category_theory.limits.reflects_colimit K₂ F

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

Equations
source
def category_theory.limits.reflects_colimit_of_nat_iso {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 G : C ⥤ D} (h : F ≅ G) [category_theory.limits.reflects_colimit K F] :
category_theory.limits.reflects_colimit K G

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

Equations
source
def category_theory.limits.reflects_colimits_of_shape_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.reflects_colimits_of_shape J F] :
category_theory.limits.reflects_colimits_of_shape J G

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

Equations
source
def category_theory.limits.reflects_colimits_of_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (h : F ≅ G) [category_theory.limits.reflects_colimits_of_size F] :
category_theory.limits.reflects_colimits_of_size G

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

Equations
source
def category_theory.limits.reflects_colimits_of_shape_of_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {J' : Type w₂} [category_theory.category J'] (e : J ≌ J') (F : C ⥤ D) [category_theory.limits.reflects_colimits_of_shape J F] :
category_theory.limits.reflects_colimits_of_shape J' F

Transfer reflection of colimits along a equivalence in the shape.

Equations
source
def category_theory.limits.reflects_colimits_of_size_shrink {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.reflects_colimits_of_size F] :
category_theory.limits.reflects_colimits_of_size F

reflects_colimits_of_size_shrink.{w w'} F tries to obtain reflects_colimits_of_size.{w w'} F from some other reflects_colimits_of_size F.

Equations
source
def category_theory.limits.reflects_smallest_colimits_of_reflects_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.reflects_colimits_of_size F] :
category_theory.limits.reflects_colimits_of_size F

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

Equations
source
noncomputable def category_theory.limits.reflects_colimit_of_reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] (F : J ⥤ C) (G : C ⥤ D) [category_theory.reflects_isomorphisms G] [category_theory.limits.has_colimit F] [category_theory.limits.preserves_colimit F G] :
category_theory.limits.reflects_colimit F G

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

Equations
source
noncomputable def category_theory.limits.reflects_colimits_of_shape_of_reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type w} [category_theory.category J] {G : C ⥤ D} [category_theory.reflects_isomorphisms G] [category_theory.limits.has_colimits_of_shape J C] [category_theory.limits.preserves_colimits_of_shape J G] :
category_theory.limits.reflects_colimits_of_shape J G

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

Equations
source
noncomputable def category_theory.limits.reflects_colimits_of_reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {G : C ⥤ D} [category_theory.reflects_isomorphisms G] [category_theory.limits.has_colimits_of_size C] [category_theory.limits.preserves_colimits_of_size G] :
category_theory.limits.reflects_colimits_of_size G

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

Equations
source
def category_theory.limits.fully_faithful_reflects_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.full F] [category_theory.faithful F] :
category_theory.limits.reflects_limits_of_size F

A fully faithful functor reflects limits.

Equations
source
def category_theory.limits.fully_faithful_reflects_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.full F] [category_theory.faithful F] :
category_theory.limits.reflects_colimits_of_size F

A fully faithful functor reflects colimits.

Equations