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.preservesLimitsOfShape {J : Type u_1} {C : Type u_2} (K : Type u_3) [Category.{u_5, u_3} K] [Category.{u_6, u_1} J] [Category.{u_7, 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.{u_7, u_3} K] [Category.{u_5, u_1} J] [Category.{u_6, u_2} C] (F : Functor J C) : preservesLimitsOfShape K F ↔ Limits.PreservesLimitsOfShape K F

@[reducible, inline]

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesLimitsOfShapeOfPreservesLimitsOfShapeColim {J : Type u_1} {C : Type u_2} (K : Type u_3) (K' : Type u_4) [Category.{u_7, u_3} K] [Category.{u_5, u_4} K'] [Category.{u_8, u_1} J] [Category.{u_6, u_2} 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_2} (K' : Type u_4) [Category.{u_5, u_4} K'] [Category.{u_7, u_1} J] [Category.{u_6, u_2} C] [Limits.HasColimitsOfShape K' C] [HasExactColimitsOfShape K' C] : preservesFiniteLimits.IsClosedUnderColimitsOfShape K'