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.{u_2, u_1} K]
(X : K)
:
PreservesWellOrderContinuousOfShape J ((evaluation K C).obj X)