Documentation

Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape

A structure to describe transfinite compositions #

Given a well-ordered type J and a morphism f : X ⟶ Y in a category, we introduce a structure TransfiniteCompositionOfShape J f expressing that f is a transfinite composition of shape J. This allows to extend this structure in order to require more properties or data for the morphisms F.obj j ⟶ F.obj (Order.succ j) which appear in the transfinite composition. See MorphismProperty.TransfiniteCompositionOfShape in the file MorphismProperty.TransfiniteComposition.

source
structure CategoryTheory.TransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] (J : Type w) [LinearOrder J] [OrderBot J] {X Y : C} (f : X ⟶ Y) [SuccOrder J] [WellFoundedLT J] :
Type (max (max u v) w)

Given a well-ordered type J, a morphism f : X ⟶ Y in a category C is a transfinite composition of shape J if we have a well order continuous functor F : J ⥤ C, an isomorphism F.obj ⊥ ≅ X, a colimit cocone for F whose point is Y, such that the composition X ⟶ F.obj ⊥ ⟶ Y is f.

Instances For
    source
    @[simp]
    theorem CategoryTheory.TransfiniteCompositionOfShape.fac_assoc {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (self : TransfiniteCompositionOfShape J f) {Z : C} (h : ((Functor.const J).obj Y).obj ⊥ ⟶ Z) :
    CategoryStruct.comp self.isoBot.inv (CategoryStruct.comp (self.incl.app ⊥) h) = CategoryStruct.comp f h
    source
    def CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
    TransfiniteCompositionOfShape J f'

    If f and f' are two isomorphic morphisms, and f is a transfinite composition of shape J, then f' also is.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_F {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
      (c.ofArrowIso e).F = c.F
      source
      @[simp]
      theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
      (c.ofArrowIso e).isColimit = c.isColimit.ofIsoColimit (Limits.Cocones.ext (Arrow.rightFunc.mapIso e) ⋯)
      source
      @[simp]
      theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_incl {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
      (c.ofArrowIso e).incl = CategoryStruct.comp c.incl ((Functor.const J).map e.hom.right)
      source
      @[simp]
      theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isoBot {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
      (c.ofArrowIso e).isoBot = c.isoBot ≪≫ Arrow.leftFunc.mapIso e
      source
      def CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) :
      TransfiniteCompositionOfShape (Fin (n + 1)) G.hom

      If G : ComposableArrows C n, then G.hom : G.left ⟶ G.right is a transfinite composition of shape Fin (n + 1).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) :
        (ofComposableArrows G).isColimit = Limits.colimitOfDiagramTerminal (Fin.isTerminalLast n) G
        source
        @[simp]
        theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) :
        (ofComposableArrows G).isoBot = Iso.refl (G.obj ⊥)
        source
        @[simp]
        theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) :
        (ofComposableArrows G).F = G
        source
        @[simp]
        theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) (j : Fin (n + 1)) :
        (ofComposableArrows G).incl.app j = G.map ((Fin.isTerminalLast n).from j)
        source
        def CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) :
        TransfiniteCompositionOfShape J' f

        If f is a transfinite composition of shape J, then it is also a transfinite composition of shape J' if J' ≃o J.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) :
          (c.ofOrderIso e).incl = whiskerLeft e.equivalence.functor c.incl
          source
          @[simp]
          theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) :
          (c.ofOrderIso e).isoBot = c.F.mapIso (eqToIso ⋯) ≪≫ c.isoBot
          source
          @[simp]
          theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_F {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) :
          (c.ofOrderIso e).F = e.equivalence.functor.comp c.F
          source
          @[simp]
          theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) :
          (c.ofOrderIso e).isColimit = c.isColimit.whiskerEquivalence e.equivalence
          source
          noncomputable def CategoryTheory.TransfiniteCompositionOfShape.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] :
          TransfiniteCompositionOfShape J (F.map f)

          If f is a transfinite composition of shape J, then F.map f also is provided F preserves suitable colimits.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.TransfiniteCompositionOfShape.map_incl {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] :
            (c.map F).incl = CategoryStruct.comp (whiskerRight c.incl F) (Functor.constComp J Y F).hom
            source
            @[simp]
            theorem CategoryTheory.TransfiniteCompositionOfShape.map_F {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] :
            (c.map F).F = c.F.comp F
            source
            @[simp]
            theorem CategoryTheory.TransfiniteCompositionOfShape.map_isColimit {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] :
            (c.map F).isColimit = (Limits.isColimitOfPreserves F c.isColimit).ofIsoColimit (Limits.Cocones.ext (Iso.refl (F.mapCocone { pt := Y, ι := c.incl }).pt) ⋯)
            source
            @[simp]
            theorem CategoryTheory.TransfiniteCompositionOfShape.map_isoBot {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] :
            (c.map F).isoBot = F.mapIso c.isoBot
            source
            noncomputable def CategoryTheory.TransfiniteCompositionOfShape.iic {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
            TransfiniteCompositionOfShape (↑(Set.Iic j)) (c.F.map (homOfLE ⋯))

            A transfinite composition of shape J induces a transfinite composition of shape Set.Iic j for any j : J.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) (i : ↑(Set.Iic j)) :
              (c.iic j).incl.app i = c.F.map (homOfLE ⋯)
              source
              @[simp]
              theorem CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
              (c.iic j).isoBot = Iso.refl ((⋯.functor.comp c.F).obj ⊥)
              source
              @[simp]
              theorem CategoryTheory.TransfiniteCompositionOfShape.iic_F {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
              (c.iic j).F = ⋯.functor.comp c.F
              source
              @[simp]
              theorem CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
              (c.iic j).isColimit = Limits.colimitOfDiagramTerminal Limits.isTerminalTop (⋯.functor.comp c.F)
              source
              noncomputable def CategoryTheory.TransfiniteCompositionOfShape.ici {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
              TransfiniteCompositionOfShape (↑(Set.Ici j)) (c.incl.app j)

              A transfinite composition of shape J induces a transfinite composition of shape Set.Ici j for any j : J.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
                (c.ici j).isColimit = (Functor.Final.isColimitWhiskerEquiv ⋯.functor { pt := Y, ι := c.incl }).invFun c.isColimit
                source
                @[simp]
                theorem CategoryTheory.TransfiniteCompositionOfShape.ici_F {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
                (c.ici j).F = ⋯.functor.comp c.F
                source
                @[simp]
                theorem CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
                (c.ici j).isoBot = Iso.refl ((⋯.functor.comp c.F).obj ⊥)
                source
                @[simp]
                theorem CategoryTheory.TransfiniteCompositionOfShape.ici_incl {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) :
                (c.ici j).incl = whiskerLeft ⋯.functor c.incl