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_3} {K : Type u_5} [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] {F F' : Functor K J} (e : F ≅ F') : preservesLimit F = preservesLimit F'

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesColimit {J : Type u_1} {C : Type u_3} {K : Type u_5} [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] {F F' : Functor K J} (e : F ≅ F') : preservesColimit F = preservesColimit F'

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesLimitsOfShape {J : Type u_1} {C : Type u_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] (F : Functor J C) : preservesLimitsOfShape K F ↔ Limits.PreservesLimitsOfShape K F

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

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

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesColimitsOfShape {J : Type u_1} {C : Type u_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} (K : Type u_5) [Category.{v_1, u_5} K] [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] (F : Functor J C) : preservesColimitsOfShape K F ↔ Limits.PreservesColimitsOfShape K F

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

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

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesFiniteLimits {J : Type u_1} {C : Type u_3} [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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_3} [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] (F : Functor J C) : preservesFiniteLimits F ↔ Limits.PreservesFiniteLimits F

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.preservesFiniteColimits {J : Type u_1} {C : Type u_3} [Category.{v_3, u_1} J] [Category.{v_5, u_3} 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

@[simp]

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesLimitsOfShapeOfPreservesLimitsOfShapeColim {J : Type u_1} {C : Type u_3} (K : Type u_5) (K' : Type u_6) [Category.{v_1, u_5} K] [Category.{v_2, u_6} K'] [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] [Limits.HasColimitsOfShape K' C] [Limits.PreservesLimitsOfShape K Limits.colim] : (preservesLimitsOfShape K).IsClosedUnderColimitsOfShape K'

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesFiniteLimitsOfHasExactColimitsOfShape {J : Type u_1} {C : Type u_3} (K' : Type u_6) [Category.{v_2, u_6} K'] [Category.{v_3, u_1} J] [Category.{v_5, u_3} C] [Limits.HasColimitsOfShape K' C] [HasExactColimitsOfShape K' C] : preservesFiniteLimits.IsClosedUnderColimitsOfShape K'