Preservation of limits, as a property of objects in the functor category

We make the typeclass PreservesLimitsOfShape K (resp. PreservesFiniteLimits) a property of objects in the functor category J ⥤ C, and show that it is stable under colimits of shape K' when they commute to limits of shape K (resp. to finite limits).

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesLimit {J : Type u_1} {C : Type u_2} {K : Type u_3} [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) : ObjectProperty (Functor J C)

The property of objects in the functor category J ⥤ C which preserves the limit of a functor F : K ⥤ J.

Equations

• CategoryTheory.ObjectProperty.preservesLimit F = CategoryTheory.Limits.PreservesLimit F

@[simp]

theorem CategoryTheory.ObjectProperty.preservesLimit_iff {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) (G : Functor J C) : preservesLimit F G ↔ Limits.PreservesLimit F G

theorem CategoryTheory.ObjectProperty.congr_preservesLimit {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] {F F' : Functor K J} (e : F ≅ F') : preservesLimit F = preservesLimit F'

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesLimit {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) : (preservesLimit F).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsFunctorPreservesLimit {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) : (preservesLimit F).IsStableUnderRetracts

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesColimit {J : Type u_1} {C : Type u_2} {K : Type u_3} [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) : ObjectProperty (Functor J C)

The property of objects in the functor category J ⥤ C which preserves the colimit of a functor F : K ⥤ J.

Equations

• CategoryTheory.ObjectProperty.preservesColimit F = CategoryTheory.Limits.PreservesColimit F

@[simp]

theorem CategoryTheory.ObjectProperty.preservesColimit_iff {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) (G : Functor J C) : preservesColimit F G ↔ Limits.PreservesColimit F G

theorem CategoryTheory.ObjectProperty.congr_preservesColimit {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] {F F' : Functor K J} (e : F ≅ F') : preservesColimit F = preservesColimit F'

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesColimit {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) : (preservesColimit F).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsFunctorPreservesColimit {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) : (preservesColimit F).IsStableUnderRetracts

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesLimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : ObjectProperty (Functor J C)

The property of objects in the functor category J ⥤ C which preserves limits of shape K.

Equations

• CategoryTheory.ObjectProperty.preservesLimitsOfShape K = CategoryTheory.Limits.PreservesLimitsOfShape K

@[simp]

theorem CategoryTheory.ObjectProperty.preservesLimitsOfShape_iff {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor J C) : preservesLimitsOfShape K F ↔ Limits.PreservesLimitsOfShape K F

theorem CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iInf {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesLimitsOfShape K = ⨅ (F : Functor K J), preservesLimit F

@[deprecated CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iInf (since := "2026-10-31")]

theorem CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iSup {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesLimitsOfShape K = ⨅ (F : Functor K J), preservesLimit F

Alias of CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iInf.

theorem CategoryTheory.ObjectProperty.congr_preservesLimitsOfShape (J : Type u_1) (C : Type u_2) {K : Type u_3} {K' : Type u_4} [Category.{v_1, u_3} K] [Category.{v_2, u_4} K'] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (e : K ≌ K') : preservesLimitsOfShape K = preservesLimitsOfShape K'

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesLimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : (preservesLimitsOfShape K).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsFunctorPreservesLimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : (preservesLimitsOfShape K).IsStableUnderRetracts

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesColimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : ObjectProperty (Functor J C)

The property of objects in the functor category J ⥤ C which preserves colimits of shape K.

Equations

• CategoryTheory.ObjectProperty.preservesColimitsOfShape K = CategoryTheory.Limits.PreservesColimitsOfShape K

@[simp]

theorem CategoryTheory.ObjectProperty.preservesColimitsOfShape_iff {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor J C) : preservesColimitsOfShape K F ↔ Limits.PreservesColimitsOfShape K F

theorem CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iInf {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesColimitsOfShape K = ⨅ (F : Functor K J), preservesColimit F

@[deprecated CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iInf (since := "2026-10-31")]

theorem CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iSup {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesColimitsOfShape K = ⨅ (F : Functor K J), preservesColimit F

Alias of CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iInf.

theorem CategoryTheory.ObjectProperty.congr_preservesColimitsOfShape (J : Type u_1) (C : Type u_2) {K : Type u_3} {K' : Type u_4} [Category.{v_1, u_3} K] [Category.{v_2, u_4} K'] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (e : K ≌ K') : preservesColimitsOfShape K = preservesColimitsOfShape K'

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesColimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : (preservesColimitsOfShape K).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsFunctorPreservesColimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : (preservesColimitsOfShape K).IsStableUnderRetracts

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesFiniteLimits {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : ObjectProperty (Functor J C)

The property of objects in the functor category J ⥤ C which preserves finite limits.

Equations

• CategoryTheory.ObjectProperty.preservesFiniteLimits = CategoryTheory.Limits.PreservesFiniteLimits

@[simp]

theorem CategoryTheory.ObjectProperty.preservesFiniteLimits_iff {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor J C) : preservesFiniteLimits F ↔ Limits.PreservesFiniteLimits F

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesFiniteLimits {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteLimits.IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.preservesFiniteLimits_eq_iInf {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteLimits = ⨅ (K : Type), ⨅ (x : SmallCategory K), ⨅ (x_1 : FinCategory K), preservesLimitsOfShape K

@[deprecated CategoryTheory.ObjectProperty.preservesFiniteLimits_eq_iInf (since := "2026-10-31")]

theorem CategoryTheory.ObjectProperty.preservesFiniteLimits_eq_iSup {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteLimits = ⨅ (K : Type), ⨅ (x : SmallCategory K), ⨅ (x_1 : FinCategory K), preservesLimitsOfShape K

Alias of CategoryTheory.ObjectProperty.preservesFiniteLimits_eq_iInf.

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsFunctorPreservesFiniteLimits {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteLimits.IsStableUnderRetracts

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesFiniteColimits {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : ObjectProperty (Functor J C)

The property of objects in the functor category J ⥤ C which preserves finite colimits.

Equations

• CategoryTheory.ObjectProperty.preservesFiniteColimits = CategoryTheory.Limits.PreservesFiniteColimits

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesFiniteColimits {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteColimits.IsClosedUnderIsomorphisms

@[simp]

theorem CategoryTheory.ObjectProperty.preservesFiniteColimits_iff {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor J C) : preservesFiniteColimits F ↔ Limits.PreservesFiniteColimits F

theorem CategoryTheory.ObjectProperty.preservesFiniteColimits_eq_iInf {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteColimits = ⨅ (K : Type), ⨅ (x : SmallCategory K), ⨅ (x_1 : FinCategory K), preservesColimitsOfShape K

@[deprecated CategoryTheory.ObjectProperty.preservesFiniteColimits_eq_iInf (since := "2026-10-31")]

theorem CategoryTheory.ObjectProperty.preservesFiniteColimits_eq_iSup {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteColimits = ⨅ (K : Type), ⨅ (x : SmallCategory K), ⨅ (x_1 : FinCategory K), preservesColimitsOfShape K

Alias of CategoryTheory.ObjectProperty.preservesFiniteColimits_eq_iInf.

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsFunctorPreservesFiniteColimits {J : Type u_1} {C : Type u_2} [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] : preservesFiniteColimits.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesColimitOfHasColimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) (K' : Type u_4) [Category.{v_1, u_3} K] [Category.{v_2, u_4} K'] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] (F : Functor K J) [Limits.HasColimitsOfShape K' C] : (preservesColimit F).IsClosedUnderColimitsOfShape K'

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesColimitsOfShapeOfHasColimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) (K' : Type u_4) [Category.{v_1, u_3} K] [Category.{v_2, u_4} K'] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] [Limits.HasColimitsOfShape K' C] : (preservesColimitsOfShape K).IsClosedUnderColimitsOfShape K'

instance CategoryTheory.ObjectProperty.instIsClosedUnderFiniteColimitsFunctorPreservesColimitsOfShapeOfHasFiniteColimits {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{v_1, u_3} K] [Category.{v_3, u_1} J] [Category.{v_4, u_2} C] [Limits.HasFiniteColimits C] : (preservesColimitsOfShape K).IsClosedUnderFiniteColimits