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 CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} (f : X ⟶ Y) extends CategoryTheory.TransfiniteCompositionOfShape J f : Type (max (max u v) w)

Structure expressing that a morphism f : X ⟶ Y in a category C is a transfinite composition of shape J of morphisms in W : MorphismProperty C.

• F : Functor J C
• isoBot : self.F.obj ⊥ ≅ X
• isWellOrderContinuous : self.F.IsWellOrderContinuous
• incl : self.F ⟶ (Functor.const J).obj Y
• isColimit : Limits.IsColimit { pt := Y, ι := self.incl }
• fac : CategoryStruct.comp self.isoBot.inv (self.incl.app ⊥) = f
• map_mem (j : J) (hj : ¬IsMax j) : W (self.F.map (homOfLE ⋯))

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIso {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : W.TransfiniteCompositionOfShape J f'

If f and f' are two isomorphic morphisms and f is a transfinite composition of morphisms in W : MorphismProperty C, then so is f'.

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofArrowIso_toTransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : (h.ofArrowIso e).toTransfiniteCompositionOfShape = h.ofArrowIso e

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) {W' : MorphismProperty C} (hW : W ≤ W') : W'.TransfiniteCompositionOfShape J f

If W ≤ W', then transfinite compositions of shape J of morphisms in W are also transfinite composition of shape J of morphisms in W'.

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE_toTransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) {W' : MorphismProperty C} (hW : W ≤ W') : (h.ofLE hW).toTransfiniteCompositionOfShape = h.toTransfiniteCompositionOfShape

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofOrderIso {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) : W.TransfiniteCompositionOfShape J' f

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.

noncomputable def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} {W : MorphismProperty D} {F : Functor C D} [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] (h : (W.inverseImage F).TransfiniteCompositionOfShape J f) : W.TransfiniteCompositionOfShape J (F.map f)

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.

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_toTransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} {W : MorphismProperty D} {F : Functor C D} [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] (h : (W.inverseImage F).TransfiniteCompositionOfShape J f) : h.map.toTransfiniteCompositionOfShape = h.map F

noncomputable def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.iic {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) (j : J) : W.TransfiniteCompositionOfShape (↑(Set.Iic j)) (h.F.map (homOfLE ⋯))

A transfinite composition of shape J of morphisms in W induces a transfinite composition of shape Set.Iic j (for any j : J).

noncomputable def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ici {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : W.TransfiniteCompositionOfShape J f) (j : J) : W.TransfiniteCompositionOfShape (↑(Set.Ici j)) (h.incl.app j)

A transfinite composition of shape J of morphisms in W induces a transfinite composition of shape Set.Ici j (for any j : J).

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))) : W.TransfiniteCompositionOfShape (Fin (n + 1)) F.hom

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.

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))) (s : Limits.Cocone F) : (ofComposableArrows W F hF).isColimit.desc s = s.ι.app (Fin.last n)

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))) : (ofComposableArrows W F hF).isoBot.hom = CategoryStruct.id (F.obj ⊥)

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))) : (ofComposableArrows W F hF).F = F

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))) : (ofComposableArrows W F hF).isoBot.inv = CategoryStruct.id (F.obj ⊥)

@[simp]

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))) (j : Fin (n + 1)) : (ofComposableArrows W F hF).incl.app j = F.map ((Fin.isTerminalLast n).from j)

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.id {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (X : C) : W.TransfiniteCompositionOfShape (Fin 1) (CategoryStruct.id X)

The identity of any object is a transfinite composition of shape Fin 1.

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofMem {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {X Y : C} (f : X ⟶ Y) (hf : W f) : W.TransfiniteCompositionOfShape (Fin 2) f

If f : X ⟶ Y satisfies W f, then f is a transfinite composition of shape Fin 2 of morphisms in W.

def CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComp {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) : W.TransfiniteCompositionOfShape (Fin 3) (CategoryStruct.comp f g)

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.

instance CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (isomorphisms C).TransfiniteCompositionOfShape J f) {j : J} (g : ⊥ ⟶ j) : IsIso (h.F.map g)

instance CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF_1 {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (isomorphisms C).TransfiniteCompositionOfShape J f) {j j' : J} (f✝ : j ⟶ j') : IsIso (h.F.map f✝)

instance CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoAppIncl {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (isomorphisms C).TransfiniteCompositionOfShape J f) (j : J) : IsIso (h.incl.app j)

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.isIso {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (isomorphisms C).TransfiniteCompositionOfShape J f) : IsIso f

A transfinite composition of isomorphisms is an isomorphism.

def CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : MorphismProperty C

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.

theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone {C : Type u} [Category.{v, u} C] (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : Monotone fun (W : MorphismProperty C) => W.transfiniteCompositionsOfShape J

theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {J' : Type w'} [LinearOrder J'] [SuccOrder J'] [OrderBot J'] [WellFoundedLT J'] (e : J ≃o J') : W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'

instance CategoryTheory.MorphismProperty.instRespectsIsoTransfiniteCompositionsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : (W.transfiniteCompositionsOfShape J).RespectsIso

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mem {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} (f : X ⟶ Y) (h : W.TransfiniteCompositionOfShape J f) : W.transfiniteCompositionsOfShape J f

theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_map_of_preserves {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] (G : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J G] {X Y : C} (f : X ⟶ Y) {P : MorphismProperty D} [Limits.PreservesColimitsOfShape J G] (h : (P.inverseImage G).transfiniteCompositionsOfShape J f) : P.transfiniteCompositionsOfShape J (G.map f)

class CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : Prop

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.

• le : W.transfiniteCompositionsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.transfiniteCompositionsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] [W.IsStableUnderTransfiniteCompositionOfShape J] : W.transfiniteCompositionsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {J' : Type w'} [LinearOrder J'] [SuccOrder J'] [OrderBot J'] [WellFoundedLT J'] (e : J ≃o J') : W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.IsStableUnderTransfiniteCompositionOfShape J'

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.IsStableUnderInfiniteComposition {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

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.

class CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

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

instance CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instIsomorphisms {C : Type u} [Category.{v, u} C] : (isomorphisms C).IsStableUnderTransfiniteComposition

theorem CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.shrink {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderTransfiniteComposition] [UnivLE.{w, w'}] : W.IsStableUnderTransfiniteComposition

theorem CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.shrink₀ {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderTransfiniteComposition] : W.IsStableUnderTransfiniteComposition

instance CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instIsMultiplicative {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderTransfiniteComposition] : W.IsMultiplicative

def CategoryTheory.MorphismProperty.transfiniteCompositions {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : MorphismProperty C

The class of transfinite compositions (for arbitrary well-ordered types J : Type w) of a class of morphisms W.

theorem CategoryTheory.MorphismProperty.transfiniteCompositions_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {X Y : C} (f : X ⟶ Y) : transfiniteCompositions.{w, v, u} W f ↔ ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f

theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : W.transfiniteCompositionsOfShape J ≤ transfiniteCompositions.{w, v, u} W

theorem CategoryTheory.MorphismProperty.transfiniteCompositions_monotone {C : Type u} [Category.{v, u} C] : Monotone transfiniteCompositions.{w, v, u}

theorem CategoryTheory.MorphismProperty.le_transfiniteCompositions {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W ≤ transfiniteCompositions.{w, v, u} W

theorem CategoryTheory.MorphismProperty.transfiniteCompositions_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderTransfiniteComposition] : transfiniteCompositions.{w, v, u} W ≤ W

@[simp]

theorem CategoryTheory.MorphismProperty.transfiniteCompositions_le_iff {C : Type u} [Category.{v, u} C] {P Q : MorphismProperty C} [Q.IsStableUnderTransfiniteComposition] : transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q