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.)

def CategoryTheory.Functor.restrictionLT {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) (j : J) : CategoryTheory.Functor (↑(Set.Iio j)) C

Given a functor F : J ⥤ C and m : J, this is the induced functor Set.Iio j ⥤ C.

Equations

• F.restrictionLT j = (Monotone.functor ⋯).comp F

@[simp]

theorem CategoryTheory.Functor.restrictionLT_map {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) (j : J) {X✝ Y✝ : ↑(Set.Iio j)} (f : X✝ ⟶ Y✝) : (F.restrictionLT j).map f = F.map ((Monotone.functor ⋯).map f)

@[simp]

theorem CategoryTheory.Functor.restrictionLT_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) (j : J) (X : ↑(Set.Iio j)) : (F.restrictionLT j).obj X = F.obj ↑X

def CategoryTheory.Functor.coconeLT {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) (m : J) : CategoryTheory.Limits.Cocone (F.restrictionLT m)

Given a functor F : J ⥤ C and m : J, this is the cocone with point F.obj m for the restriction of F to Set.Iio m.

Equations

• F.coconeLT m = { pt := F.obj m, ι := { app := fun (x : ↑(Set.Iio m)) => match x with | ⟨i, hi⟩ => F.map (CategoryTheory.homOfLE ⋯), naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Functor.coconeLT_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) (m : J) (x✝ : ↑(Set.Iio m)) : (F.coconeLT m).ι.app x✝ = match x✝ with | ⟨i, hi⟩ => F.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem CategoryTheory.Functor.coconeLT_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) (m : J) : (F.coconeLT m).pt = F.obj m

class CategoryTheory.Functor.IsWellOrderContinuous {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) : Prop

A functor F : J ⥤ C is well-order-continuous if for any limit element m : J, F.obj m identifies to the colimit of the F.obj j for j < m.

• nonempty_isColimit (m : J) (hm : Order.IsSuccLimit m) : Nonempty (CategoryTheory.Limits.IsColimit (F.coconeLT m))

noncomputable def CategoryTheory.Functor.isColimitOfIsWellOrderContinuous {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] (F : CategoryTheory.Functor J C) [F.IsWellOrderContinuous] (m : J) (hm : Order.IsSuccLimit m) : CategoryTheory.Limits.IsColimit (F.coconeLT m)

If F : J ⥤ C is well-order-continuous and m : J is a limit element, then the cocone F.coconeLT m is colimit, i.e. F.obj m identifies to the colimit of the F.obj j for j < m.

Equations

• F.isColimitOfIsWellOrderContinuous m hm = ⋯.some

instance CategoryTheory.Functor.instIsWellOrderContinuousNat {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor ℕ C) : F.IsWellOrderContinuous

theorem CategoryTheory.Functor.isWellOrderContinuous_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [Preorder J] {F G : CategoryTheory.Functor J C} (e : F ≅ G) [F.IsWellOrderContinuous] : G.IsWellOrderContinuous

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

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

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.IsStableUnderInfiniteComposition {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.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 (CategoryTheory.CategoryStruct.id X)
• comp_mem {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
• isStableUnderTransfiniteCompositionOfShape (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] : W.IsStableUnderTransfiniteCompositionOfShape J