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) : Prop

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

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

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) : Prop

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

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

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) : Prop

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.

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

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) : Prop

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.

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

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) : Prop

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

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

@[reducible, inline]

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) : Prop

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

Equations

• CategoryTheory.Limits.PreservesLimits F = CategoryTheory.Limits.PreservesLimitsOfSize.{?u.36, ?u.36, ?u.37, ?u.36, ?u.35, ?u.34} F

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) : Prop

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

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

@[reducible, inline]

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) : Prop

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

Equations

• CategoryTheory.Limits.PreservesColimits F = CategoryTheory.Limits.PreservesColimitsOfSize.{?u.36, ?u.36, ?u.37, ?u.36, ?u.35, ?u.34} F

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.

Equations

• CategoryTheory.Limits.isLimitOfPreserves F t = ⋯.some

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.

Equations

• CategoryTheory.Limits.isColimitOfPreserves F t = ⋯.some

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.preservesLimitsOfSize_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)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.preservesColimitsOfSize_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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[deprecated]

theorem 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.id_preservesColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)

Equations

• ⋯ = ⋯

@[deprecated]

theorem 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.instHasLimitCompOfPreservesLimit {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} [CategoryTheory.Limits.HasLimit K] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesLimit K F] : CategoryTheory.Limits.HasLimit (K.comp F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.instHasColimitCompOfPreservesColimit {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} [CategoryTheory.Limits.HasColimit K] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesColimit K F] : CategoryTheory.Limits.HasColimit (K.comp F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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} {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 (K.comp F) G] : CategoryTheory.Limits.PreservesLimit K (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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] {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 (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_preservesLimits {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₃} (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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} {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 (K.comp F) G] : CategoryTheory.Limits.PreservesColimit K (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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] {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 (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_preservesColimits {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₃} (F.comp G)

Equations

• ⋯ = ⋯

@[deprecated]

theorem 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 (K.comp F) G] : CategoryTheory.Limits.PreservesLimit K (F.comp G)

@[deprecated]

theorem 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 (F.comp G)

@[deprecated]

theorem 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₃} (F.comp G)

@[deprecated]

theorem 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 (K.comp F) G] : CategoryTheory.Limits.PreservesColimit K (F.comp G)

@[deprecated]

theorem 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 (F.comp G)

@[deprecated]

theorem 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₃} (F.comp G)

theorem CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone {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.

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.preservesLimit_of_iso_diagram {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₁ 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.

@[deprecated]

theorem 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₁ K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.PreservesLimit K₁ F] : CategoryTheory.Limits.PreservesLimit K₂ F

theorem CategoryTheory.Limits.preservesLimit_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesLimit K F] : CategoryTheory.Limits.PreservesLimit K G

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.Limits.PreservesLimitsOfShape J G

theorem CategoryTheory.Limits.preservesLimits_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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.

@[deprecated]

theorem CategoryTheory.Limits.preservesLimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_equiv {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.

@[deprecated]

theorem 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

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

A functor preserving larger limits also preserves smaller limits.

@[deprecated]

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_shrink {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

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

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits {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.

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone {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.

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.preservesColimit_of_iso_diagram {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₁ 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.

@[deprecated]

theorem 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₁ K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.PreservesColimit K₁ F] : CategoryTheory.Limits.PreservesColimit K₂ F

theorem CategoryTheory.Limits.preservesColimit_of_natIso {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 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.

@[deprecated CategoryTheory.Limits.preservesColimit_of_natIso]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesColimit K F] : CategoryTheory.Limits.PreservesColimit K G

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesColimitsOfShape J F] : CategoryTheory.Limits.PreservesColimitsOfShape J G

theorem CategoryTheory.Limits.preservesColimits_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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.

@[deprecated]

theorem CategoryTheory.Limits.preservesColimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_equiv {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.

@[deprecated]

theorem 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

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

A functor preserving larger colimits also preserves smaller colimits.

@[deprecated]

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_shrink {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

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

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits {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.

@[deprecated]

theorem 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

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) : Prop

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.

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

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) : Prop

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.

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

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) : Prop

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.

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

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) : Prop

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.

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

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) : Prop

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.

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

@[reducible, inline]

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) : Prop

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.

Equations

• CategoryTheory.Limits.ReflectsLimits F = CategoryTheory.Limits.ReflectsLimitsOfSize.{?u.36, ?u.36, ?u.37, ?u.36, ?u.35, ?u.34} F

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) : Prop

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.

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

@[reducible, inline]

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) : Prop

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.

Equations

• CategoryTheory.Limits.ReflectsColimits F = CategoryTheory.Limits.ReflectsColimitsOfSize.{?u.36, ?u.36, ?u.37, ?u.36, ?u.35, ?u.34} F

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.

Equations

• CategoryTheory.Limits.isLimitOfReflects F t = ⋯.some

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.

Equations

• CategoryTheory.Limits.isColimitOfReflects F t = ⋯.some

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.reflectsLimit_of_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] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimit K F

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.reflectsColimit_of_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] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfShape J F] : CategoryTheory.Limits.ReflectsColimit K F

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits {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

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits {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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[deprecated]

theorem 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.id_reflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)

Equations

• ⋯ = ⋯

@[deprecated]

theorem 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.comp_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} {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 (K.comp F) G] : CategoryTheory.Limits.ReflectsLimit K (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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] {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 (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_reflectsLimits {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₃} (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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} {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 (K.comp F) G] : CategoryTheory.Limits.ReflectsColimit K (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_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] {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 (F.comp G)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.comp_reflectsColimits {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₃} (F.comp G)

Equations

• ⋯ = ⋯

@[deprecated]

theorem 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 (K.comp F) G] : CategoryTheory.Limits.ReflectsLimit K (F.comp G)

@[deprecated]

theorem 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 (F.comp G)

@[deprecated]

theorem 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₃} (F.comp G)

@[deprecated]

theorem 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 (K.comp F) G] : CategoryTheory.Limits.ReflectsColimit K (F.comp G)

@[deprecated]

theorem 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 (F.comp G)

@[deprecated]

theorem 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₃} (F.comp G)

theorem CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves {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.comp G)] [CategoryTheory.Limits.ReflectsLimit (K.comp 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.

@[deprecated]

theorem 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 (F.comp G)] [CategoryTheory.Limits.ReflectsLimit (K.comp F) G] : CategoryTheory.Limits.PreservesLimit K F

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves {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.comp 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.

@[deprecated]

theorem 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 (F.comp G)] [CategoryTheory.Limits.ReflectsLimitsOfShape J G] : CategoryTheory.Limits.PreservesLimitsOfShape J F

theorem CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves {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.comp 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.

@[deprecated]

theorem 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₃} (F.comp G)] [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F

theorem CategoryTheory.Limits.reflectsLimit_of_iso_diagram {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₁ 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.

@[deprecated]

theorem 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₁ K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.ReflectsLimit K₁ F] : CategoryTheory.Limits.ReflectsLimit K₂ F

theorem CategoryTheory.Limits.reflectsLimit_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimit K F] : CategoryTheory.Limits.ReflectsLimit K G

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsLimitsOfShape J F] : CategoryTheory.Limits.ReflectsLimitsOfShape J G

theorem CategoryTheory.Limits.reflectsLimits_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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.

@[deprecated]

theorem CategoryTheory.Limits.reflectsLimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv {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.

@[deprecated]

theorem 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

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

A functor reflecting larger limits also reflects smaller limits.

@[deprecated]

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

theorem CategoryTheory.Limits.reflectsLimitsOfSize_shrink {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

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

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.reflectsSmallestLimits_of_reflectsLimits {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.

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms {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) [G.ReflectsIsomorphisms] [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.

@[deprecated]

theorem 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) [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasLimit F] [CategoryTheory.Limits.PreservesLimit F G] : CategoryTheory.Limits.ReflectsLimit F G

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms {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} [G.ReflectsIsomorphisms] [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.

@[deprecated]

theorem 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} [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.PreservesLimitsOfShape J G] : CategoryTheory.Limits.ReflectsLimitsOfShape J G

theorem CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms] [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.

@[deprecated]

theorem CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms] [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

theorem CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves {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.comp G)] [CategoryTheory.Limits.ReflectsColimit (K.comp 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.

@[deprecated]

theorem 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 (F.comp G)] [CategoryTheory.Limits.ReflectsColimit (K.comp F) G] : CategoryTheory.Limits.PreservesColimit K F

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves {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.comp 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.

@[deprecated]

theorem 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 (F.comp G)] [CategoryTheory.Limits.ReflectsColimitsOfShape J G] : CategoryTheory.Limits.PreservesColimitsOfShape J F

theorem CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves {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.comp 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.

@[deprecated]

theorem 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₃} (F.comp G)] [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G] : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F

theorem CategoryTheory.Limits.reflectsColimit_of_iso_diagram {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₁ 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.

@[deprecated]

theorem 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₁ K₂ : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.ReflectsColimit K₁ F] : CategoryTheory.Limits.ReflectsColimit K₂ F

theorem CategoryTheory.Limits.reflectsColimit_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsColimit K F] : CategoryTheory.Limits.ReflectsColimit K G

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_natIso {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 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.

@[deprecated]

theorem 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 G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsColimitsOfShape J F] : CategoryTheory.Limits.ReflectsColimitsOfShape J G

theorem CategoryTheory.Limits.reflectsColimits_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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.

@[deprecated]

theorem CategoryTheory.Limits.reflectsColimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv {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.

@[deprecated]

theorem 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

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

A functor reflecting larger colimits also reflects smaller colimits.

@[deprecated]

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

theorem CategoryTheory.Limits.reflectsColimitsOfSize_shrink {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

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

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits {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.

@[deprecated]

theorem 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

theorem CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms {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) [G.ReflectsIsomorphisms] [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.

@[deprecated]

theorem 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) [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.PreservesColimit F G] : CategoryTheory.Limits.ReflectsColimit F G

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms {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} [G.ReflectsIsomorphisms] [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.

@[deprecated]

theorem 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} [G.ReflectsIsomorphisms] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.PreservesColimitsOfShape J G] : CategoryTheory.Limits.ReflectsColimitsOfShape J G

theorem CategoryTheory.Limits.reflectsColimits_of_reflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms] [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.

@[deprecated]

theorem CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms] [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

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

A fully faithful functor reflects limits.

Equations

• ⋯ = ⋯

@[deprecated]

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

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

A fully faithful functor reflects colimits.

Equations

• ⋯ = ⋯

@[deprecated]

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