Classes of morphisms that are stable under transfinite composition

Let F : J ⥤ C be a functor from a well ordered type J. We say that F is well-order-continuous (F.IsWellOrderContinuous), if for any m : J which satisfies hm : Order.IsSuccLimit m, F.obj m identifies to the colimit of the F.obj j for j < m.

Given W : MorphismProperty C, we say that W.IsStableUnderTransfiniteCompositionOfShape J if for any colimit cocone c for a well-order-continuous functor F : J ⥤ C such that F.obj j ⟶ F.obj (Order.succ j) belongs to W, we can conclude that c.ι.app ⊥ : F.obj ⊥ ⟶ c.pt belongs to W. The morphisms of this form c.ι.app ⊥ for any F and c are part of the morphism property W.transfiniteCompositionsOfShape J. The condition of being stable by transfinite composition of shape J is actually phrased as W.transfiniteCompositionsOfShape J ≤ W.

In particular, if J := ℕ, we define W.IsStableUnderInfiniteComposition, which means that if F : ℕ ⥤ C is such that F.obj n ⟶ F.obj (n + 1) belongs to W, then F.obj 0 ⟶ c.pt belongs to W for any colimit cocone c : Cocone F.

Finally, we define the class W.IsStableUnderTransfiniteComposition which says that W.IsStableUnderTransfiniteCompositionOfShape J holds for any well ordered type J in a certain universe u. (We also require that W is multiplicative.)

inductive 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, we say that a morphism in C is a transfinite composition of morphisms in W of shape J if it is of the form c.ι.app ⊥ : F.obj ⊥ ⟶ c.pt where c is a colimit cocone for a well-order-continuous functor F : J ⥤ C such that for any non-maximal j : J, the map F.map j ⟶ F.map (Order.succ j) is in W.

• mk {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] (F : Functor J C) [F.IsWellOrderContinuous] (hF : ∀ (j : J), ¬IsMax j → W (F.map (homOfLE ⋯))) (c : Limits.Cocone F) (hc : Limits.IsColimit c) : W.transfiniteCompositionsOfShape J (c.ι.app ⊥)

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.RespectsIso] : (W.transfiniteCompositionsOfShape J).RespectsIso

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.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.mem_of_transfinite_composition {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] [W.IsStableUnderTransfiniteCompositionOfShape J] {F : Functor J C} [F.IsWellOrderContinuous] (hF : ∀ (j : J), ¬IsMax j → W (F.map (homOfLE ⋯))) {c : Limits.Cocone F} (hc : Limits.IsColimit c) : W (c.ι.app ⊥)

@[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.

Equations

• W.IsStableUnderInfiniteComposition = W.IsStableUnderTransfiniteCompositionOfShape ℕ

class CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) extends W.IsMultiplicative : 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).

• id_mem (X : C) : W (CategoryStruct.id X)
• comp_mem {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W f → W g → W (CategoryStruct.comp f g)
• isStableUnderTransfiniteCompositionOfShape (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : W.IsStableUnderTransfiniteCompositionOfShape J