Preservation of well order continuous functors #
Given a well-ordered type J and a functor G : C ⥤ D,
we define a type class PreservesWellOrderContinuousOfShape J G
saying that G preserves colimits of shape Set.Iio j
for any limit element j : J. It follows that if
F : J ⥤ C is well order continuous, then so is F ⋙ G.
class CategoryTheory.Limits.PreservesWellOrderContinuousOfShape {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (J : Type w) [LinearOrder J] (G : Functor C D) :
A functor G : C ⥤ D satisfies PreservesWellOrderContinuousOfShape J G
if for any limit element j in the preordered type J, the functor G
preserves colimits of shape Set.Iio j.
- preservesColimitsOfShape (j : J) (hj : Order.IsSuccLimit j) : PreservesColimitsOfShape (↑(Set.Iio j)) G
Instances
theorem CategoryTheory.Limits.preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] {J : Type w} [LinearOrder J] (G : Functor C D) [PreservesWellOrderContinuousOfShape J G] (j : J) (hj : Order.IsSuccLimit j) :
PreservesColimitsOfShape (↑(Set.Iio j)) G
instance CategoryTheory.Limits.instIsWellOrderContinuousCompOfPreservesWellOrderContinuousOfShape {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (J : Type w) [LinearOrder J] (F : Functor J C) (G : Functor C D) [F.IsWellOrderContinuous] [PreservesWellOrderContinuousOfShape J G] :
(F.comp G).IsWellOrderContinuous
instance CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeComp {C : Type u} {D : Type u'} {E : Type u''} [Category.{v, u} C] [Category.{v', u'} D] [Category.{v'', u''} E] (J : Type w) [LinearOrder J] (G₁ : Functor C D) (G₂ : Functor D E) [PreservesWellOrderContinuousOfShape J G₁] [PreservesWellOrderContinuousOfShape J G₂] :
PreservesWellOrderContinuousOfShape J (G₁.comp G₂)
instance CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeFunctorObjEvaluationOfHasIterationOfShape {C : Type u} [Category.{v, u} C] (J : Type w) [LinearOrder J] [HasIterationOfShape J C] (K : Type u_1) [Category.{v_1, u_1} K] (X : K) :
PreservesWellOrderContinuousOfShape J ((evaluation K C).obj X)