Documentation

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

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

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.

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
      @[reducible, inline]

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

        Instances