Classes of morphisms that are stable under transfinite composition #
Given a well ordered type J
, W : MorphismProperty C
and
a morphism f : X ⟶ Y
, we define a structure W.TransfiniteCompositionOfShape J f
which expresses that f
is a transfinite composition of shape J
of morphisms in W
.
This structures extends CategoryTheory.TransfiniteCompositionOfShape
which was
defined in the file CategoryTheory.Limits.Shape.Preorder.TransfiniteCompositionOfShape
.
We use this structure in order to define the class of morphisms
W.transfiniteCompositionsOfShape J : MorphismProperty C
, and the type class
W.IsStableUnderTransfiniteCompositionOfShape J
.
In particular, if J := ℕ
, we define W.IsStableUnderInfiniteComposition
,
Finally, we introduce the class W.IsStableUnderTransfiniteComposition
which says that W.IsStableUnderTransfiniteCompositionOfShape J
holds for any well ordered type J
in a certain universe w
.
Structure expressing that a morpshism f : X ⟶ Y
in a category C
is a transfinite composition of shape J
of morphisms in W : MorphismProperty C
.
- isColimit : Limits.IsColimit { pt := Y, ι := self.incl }
Instances For
If f
and f'
are two isomorphic morphisms and f
is a transfinite composition
of morphisms in W : MorphismProperty C
, then so is f'
.
Equations
- h.ofArrowIso e = { toTransfiniteCompositionOfShape := h.ofArrowIso e, map_mem := ⋯ }
Instances For
If W ≤ W'
, then transfinite compositions of shape J
of morphisms in W
are also transfinite composition of shape J
of morphisms in W'
.
Equations
- h.ofLE hW = { toTransfiniteCompositionOfShape := h.toTransfiniteCompositionOfShape, map_mem := ⋯ }
Instances For
If f
is a transfinite composition of shape J
of morphisms in W
,
then it is also a transfinite composition of shape J'
of morphisms in W
if J' ≃o J
.
Equations
- h.ofOrderIso e = { toTransfiniteCompositionOfShape := h.ofOrderIso e, map_mem := ⋯ }
Instances For
If f
is a transfinite composition of shape J
of morphisms
in W.inverseImage F
, then F
is a transfinite composition of shape J
of morphisms in W
provided F
preserves suitable colimits.
Instances For
A transfinite composition of shape J
of morphisms in W
induces a transfinite
composition of shape Set.Iic j
(for any j : J
).
Instances For
A transfinite composition of shape J
of morphisms in W
induces a transfinite
composition of shape Set.Ici j
(for any j : J
).
Instances For
If F : ComposableArrows C n
and all maps F.obj i.castSucc ⟶ F.obj i.succ
are in W
, then F.hom : F.left ⟶ F.right
is a transfinite composition of
shape Fin (n + 1)
of morphisms in W
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity of any object is a transfinite composition of shape Fin 1
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f : X ⟶ Y
satisfies W f
, then f
is a transfinite composition of shape Fin 2
of morphisms in W
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f : X ⟶ Y
and g : Y ⟶ Z
satisfy W f
and W g
, then f ≫ g
is a
transfinite composition of shape Fin 3
of morphisms in W
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A transfinite composition of isomorphisms is an isomorphism.
Given W : MorphismProperty C
and a well-ordered type J
, this is
the class of morphisms that are transfinite composition of shape J
of morphisms in W
.
Equations
- W.transfiniteCompositionsOfShape J f = Nonempty (W.TransfiniteCompositionOfShape J f)
Instances For
A class of morphisms W : MorphismProperty C
is stable under transfinite compositions
of shape J
if for any well-order-continuous functor F : J ⥤ C
such that
F.obj j ⟶ F.obj (Order.succ j)
is in W
, then F.obj ⊥ ⟶ c.pt
is in W
for any colimit cocone c : Cocone F
.
Instances
A class of morphisms W : MorphismProperty C
is stable under infinite composition
if for any functor F : ℕ ⥤ C
such that F.obj n ⟶ F.obj (n + 1)
is in W
for any n : ℕ
,
the map F.obj 0 ⟶ c.pt
is in W
for any colimit cocone c : Cocone F
.
Instances For
A class of morphisms W : MorphismProperty C
is stable under transfinite composition
if it is multiplicative and stable under transfinite composition of any shape
(in a certain universe).
- isStableUnderTransfiniteCompositionOfShape (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : W.IsStableUnderTransfiniteCompositionOfShape J
Instances
The class of transfinite compositions (for arbitrary well-ordered types J : Type w
)
of a class of morphisms W
.
Equations
- One or more equations did not get rendered due to their size.