Documentation

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

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.

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

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

                          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.
                          Instances For