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

• preserves : {c : CategoryTheory.Limits.Cone K} → CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (F.mapCone c)

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

class CategoryTheory.Limits.PreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Type (max (max (max (max u₁ u₂) v₁) v₂) w)

• preserves : {c : CategoryTheory.Limits.Cocone K} → CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (F.mapCocone c)

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

class CategoryTheory.Limits.PreservesLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

• preservesLimit : {K : CategoryTheory.Functor J C} → CategoryTheory.Limits.PreservesLimit K F

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.

class CategoryTheory.Limits.PreservesColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

• preservesColimit : {K : CategoryTheory.Functor J C} → CategoryTheory.Limits.PreservesColimit K F

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.

class CategoryTheory.Limits.PreservesLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

• preservesLimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.PreservesLimitsOfShape J F

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

@[inline, reducible]

abbrev CategoryTheory.Limits.PreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : 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.

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

• preservesColimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.PreservesColimitsOfShape J F

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

@[inline, reducible]

abbrev CategoryTheory.Limits.PreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : 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.

def CategoryTheory.Limits.isLimitOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cone K} (t : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Limits.PreservesLimit K F] : CategoryTheory.Limits.IsLimit (F.mapCone c)

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

def CategoryTheory.Limits.isColimitOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cocone K} (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit K F] : CategoryTheory.Limits.IsColimit (F.mapCocone c)

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

instance CategoryTheory.Limits.preservesLimit_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.PreservesLimit K F)

instance CategoryTheory.Limits.preservesColimit_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.PreservesColimit K F)

instance CategoryTheory.Limits.preservesLimitsOfShape_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.PreservesLimitsOfShape J F)

instance CategoryTheory.Limits.preservesColimitsOfShape_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.PreservesColimitsOfShape J F)

instance CategoryTheory.Limits.preserves_limits_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

instance CategoryTheory.Limits.preserves_colimits_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

instance CategoryTheory.Limits.idPreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)

instance CategoryTheory.Limits.idPreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)

instance CategoryTheory.Limits.compPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimit K F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.comp K F) G] : CategoryTheory.Limits.PreservesLimit K (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compPreservesLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F] [CategoryTheory.Limits.PreservesLimitsOfShape J G] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compPreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimit K F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp K F) G] : CategoryTheory.Limits.PreservesColimit K (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compPreservesColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J F] [CategoryTheory.Limits.PreservesColimitsOfShape J G] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compPreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (CategoryTheory.Functor.comp F G)

def CategoryTheory.Limits.preservesLimitOfPreservesLimitCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cone K} (h : CategoryTheory.Limits.IsLimit t) (hF : CategoryTheory.Limits.IsLimit (F.mapCone t)) : CategoryTheory.Limits.PreservesLimit K F

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

def CategoryTheory.Limits.preservesLimitOfIsoDiagram {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K₁ : CategoryTheory.Functor J C} {K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.PreservesLimit K₁ F] : CategoryTheory.Limits.PreservesLimit K₂ F

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

def CategoryTheory.Limits.preservesLimitOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesLimit K F] : CategoryTheory.Limits.PreservesLimit K G

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

def CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.Limits.PreservesLimitsOfShape J G

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

def CategoryTheory.Limits.preservesLimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

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

def CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {J' : Type w₂} [CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.Limits.PreservesLimitsOfShape J' F

Transfer preservation of limits along an equivalence in the shape.

def CategoryTheory.Limits.preservesLimitsOfSizeShrink {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cocone K} (h : CategoryTheory.Limits.IsColimit t) (hF : CategoryTheory.Limits.IsColimit (F.mapCocone t)) : CategoryTheory.Limits.PreservesColimit K F

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

def CategoryTheory.Limits.preservesColimitOfIsoDiagram {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K₁ : CategoryTheory.Functor J C} {K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.PreservesColimit K₁ F] : CategoryTheory.Limits.PreservesColimit K₂ F

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

def CategoryTheory.Limits.preservesColimitOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesColimit K F] : CategoryTheory.Limits.PreservesColimit K G

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

def CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.Limits.PreservesColimitsOfShape J G

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

def CategoryTheory.Limits.preservesColimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

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

def CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {J' : Type w₂} [CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.Limits.PreservesColimitsOfShape J' F

Transfer preservation of colimits along an equivalence in the shape.

def CategoryTheory.Limits.preservesColimitsOfSizeShrink {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

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

class CategoryTheory.Limits.ReflectsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Type (max (max (max (max u₁ u₂) v₁) v₂) w)

• reflects : {c : CategoryTheory.Limits.Cone K} → CategoryTheory.Limits.IsLimit (F.mapCone c) → CategoryTheory.Limits.IsLimit c

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.

class CategoryTheory.Limits.ReflectsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Type (max (max (max (max u₁ u₂) v₁) v₂) w)

• reflects : {c : CategoryTheory.Limits.Cocone K} → CategoryTheory.Limits.IsColimit (F.mapCocone c) → CategoryTheory.Limits.IsColimit c

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.

class CategoryTheory.Limits.ReflectsLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

• reflectsLimit : {K : CategoryTheory.Functor J C} → CategoryTheory.Limits.ReflectsLimit K F

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.

class CategoryTheory.Limits.ReflectsColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')

• reflectsColimit : {K : CategoryTheory.Functor J C} → CategoryTheory.Limits.ReflectsColimit K F

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.

class CategoryTheory.Limits.ReflectsLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

• reflectsLimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.ReflectsLimitsOfShape J F

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.

@[inline, reducible]

abbrev CategoryTheory.Limits.ReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : 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.

class CategoryTheory.Limits.ReflectsColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

• reflectsColimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.ReflectsColimitsOfShape J F

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.

@[inline, reducible]

abbrev CategoryTheory.Limits.ReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : 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.

def CategoryTheory.Limits.isLimitOfReflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cone K} (t : CategoryTheory.Limits.IsLimit (F.mapCone c)) [CategoryTheory.Limits.ReflectsLimit K F] : CategoryTheory.Limits.IsLimit c

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

def CategoryTheory.Limits.isColimitOfReflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cocone K} (t : CategoryTheory.Limits.IsColimit (F.mapCocone c)) [CategoryTheory.Limits.ReflectsColimit K F] : CategoryTheory.Limits.IsColimit c

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

instance CategoryTheory.Limits.reflectsLimit_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.ReflectsLimit K F)

instance CategoryTheory.Limits.reflectsColimit_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.ReflectsColimit K F)

instance CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.ReflectsLimitsOfShape J F)

instance CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.ReflectsColimitsOfShape J F)

instance CategoryTheory.Limits.reflects_limits_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

instance CategoryTheory.Limits.reflects_colimits_subsingleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Subsingleton (CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

instance CategoryTheory.Limits.reflectsLimitOfReflectsLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimit K F

instance CategoryTheory.Limits.reflectsColimitOfReflectsColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfShape J F] : CategoryTheory.Limits.ReflectsColimit K F

instance CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsLimitsOfShape J F

instance CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsColimitsOfShape J F

instance CategoryTheory.Limits.idReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)

instance CategoryTheory.Limits.idReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)

instance CategoryTheory.Limits.compReflectsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimit K F] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.comp K F) G] : CategoryTheory.Limits.ReflectsLimit K (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compReflectsLimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] [CategoryTheory.Limits.ReflectsLimitsOfShape J G] : CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compReflectsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsColimit K F] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.comp K F) G] : CategoryTheory.Limits.ReflectsColimit K (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compReflectsColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsColimitsOfShape J F] [CategoryTheory.Limits.ReflectsColimitsOfShape J G] : CategoryTheory.Limits.ReflectsColimitsOfShape J (CategoryTheory.Functor.comp F G)

instance CategoryTheory.Limits.compReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (CategoryTheory.Functor.comp F G)

def CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimit K (CategoryTheory.Functor.comp F G)] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.comp K F) G] : CategoryTheory.Limits.PreservesLimit K F

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

def CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Functor.comp F G)] [CategoryTheory.Limits.ReflectsLimitsOfShape J G] : CategoryTheory.Limits.PreservesLimitsOfShape J F

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

def CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (CategoryTheory.Functor.comp F G)] [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.reflectsLimitOfIsoDiagram {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K₁ : CategoryTheory.Functor J C} {K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.ReflectsLimit K₁ F] : CategoryTheory.Limits.ReflectsLimit K₂ F

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

def CategoryTheory.Limits.reflectsLimitOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimit K F] : CategoryTheory.Limits.ReflectsLimit K G

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

def CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimitsOfShape J G

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

def CategoryTheory.Limits.reflectsLimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G

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

def CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {J' : Type w₂} [CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimitsOfShape J' F

Transfer reflection of limits along an equivalence in the shape.

def CategoryTheory.Limits.reflectsLimitsOfSizeShrink {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasLimit F] [CategoryTheory.Limits.PreservesLimit F G] : CategoryTheory.Limits.ReflectsLimit F G

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

def CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {G : CategoryTheory.Functor C D} [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.PreservesLimitsOfShape J G] : CategoryTheory.Limits.ReflectsLimitsOfShape 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.

def CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor C D} [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasLimitsOfSize.{w', w, v₁, u₁} C] [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G] : CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G

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

def CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimit K (CategoryTheory.Functor.comp F G)] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.comp K F) G] : CategoryTheory.Limits.PreservesColimit K F

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

def CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Functor.comp F G)] [CategoryTheory.Limits.ReflectsColimitsOfShape J G] : CategoryTheory.Limits.PreservesColimitsOfShape J F

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

def CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (CategoryTheory.Functor.comp F G)] [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.reflectsColimitOfIsoDiagram {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K₁ : CategoryTheory.Functor J C} {K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.ReflectsColimit K₁ F] : CategoryTheory.Limits.ReflectsColimit K₂ F

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

def CategoryTheory.Limits.reflectsColimitOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsColimit K F] : CategoryTheory.Limits.ReflectsColimit K G

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

def CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsColimitsOfShape J F] : CategoryTheory.Limits.ReflectsColimitsOfShape J G

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

def CategoryTheory.Limits.reflectsColimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

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

def CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {J' : Type w₂} [CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfShape J F] : CategoryTheory.Limits.ReflectsColimitsOfShape J' F

Transfer reflection of colimits along an equivalence in the shape.

def CategoryTheory.Limits.reflectsColimitsOfSizeShrink {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

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

def CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.PreservesColimit F G] : CategoryTheory.Limits.ReflectsColimit F G

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

def CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {G : CategoryTheory.Functor C D} [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.PreservesColimitsOfShape J G] : CategoryTheory.Limits.ReflectsColimitsOfShape 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.

def CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor C D} [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasColimitsOfSize.{w', w, v₁, u₁} C] [CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G

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

def CategoryTheory.Limits.fullyFaithfulReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] : CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

A fully faithful functor reflects limits.

def CategoryTheory.Limits.fullyFaithfulReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

A fully faithful functor reflects colimits.