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

          Equations
          • h.map = { toTransfiniteCompositionOfShape := h.map F, map_mem := }
          Instances For

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

            Equations
            • h.iic j = { toTransfiniteCompositionOfShape := h.iic j, map_mem := }
            Instances For

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

              Equations
              • h.ici j = { toTransfiniteCompositionOfShape := h.ici j, map_mem := }
              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

                        A transfinite composition of isomorphisms is an isomorphism.

                        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