Documentation

Mathlib.CategoryTheory.Sums.Associator

Associator for binary disjoint union of categories. #

The associator functor ((C ⊕ D) ⊕ E) ⥤ (C ⊕ (D ⊕ E)) and its inverse form an equivalence.

source
🔸 coverage
def CategoryTheory.sum.associator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
Functor ((C ⊕ D) ⊕ E) (C ⊕ D ⊕ E)

The associator functor (C ⊕ D) ⊕ E ⥤ C ⊕ (D ⊕ E) for sums of categories.

Instances For
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.sum.associator_obj_inl_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) :
    (associator C D E).obj (Sum.inl (Sum.inl X)) = Sum.inl X
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.sum.associator_obj_inl_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) :
    (associator C D E).obj (Sum.inl (Sum.inr X)) = Sum.inr (Sum.inl X)
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.sum.associator_obj_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) :
    (associator C D E).obj (Sum.inr X) = Sum.inr (Sum.inr X)
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.sum.associator_map_inl_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : C} (f : X ⟶ Y) :
    (associator C D E).map ((Sum.inl_ (C ⊕ D) E).map ((Sum.inl_ C D).map f)) = (Sum.inl_ C (D ⊕ E)).map f
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.sum.associator_map_inl_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : D} (f : X ⟶ Y) :
    (associator C D E).map ((Sum.inl_ (C ⊕ D) E).map ((Sum.inr_ C D).map f)) = (Sum.inr_ C (D ⊕ E)).map ((Sum.inl_ D E).map f)
    source
    📐 coverage
    @[simp]
    theorem CategoryTheory.sum.associator_map_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : E} (f : X ⟶ Y) :
    (associator C D E).map ((Sum.inr_ (C ⊕ D) E).map f) = (Sum.inr_ C (D ⊕ E)).map ((Sum.inr_ D E).map f)
    source
    🔸 coverage
    def CategoryTheory.sum.inlCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
    (Sum.inl_ (C ⊕ D) E).comp (associator C D E) ≅ (Sum.inl_ C (D ⊕ E)).sum' ((Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E)))

    Characterizing the composition of the associator and the left inclusion.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.sum.inlCompAssociator_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C ⊕ D) :
      (inlCompAssociator C D E).hom.app X = CategoryStruct.id (((Sum.inl_ C (D ⊕ E)).sum' ((Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E)))).obj X)
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.sum.inlCompAssociator_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C ⊕ D) :
      (inlCompAssociator C D E).inv.app X = CategoryStruct.id (((Sum.inl_ C (D ⊕ E)).sum' ((Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E)))).obj X)
      source
      🔸 coverage
      def CategoryTheory.sum.inrCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
      (Sum.inr_ (C ⊕ D) E).comp (associator C D E) ≅ (Sum.inr_ D E).comp (Sum.inr_ C (D ⊕ E))

      Characterizing the composition of the associator and the right inclusion.

      Instances For
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.sum.inrCompAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) :
        ((inrCompAssociator C D E).inv.app X).down.down = CategoryStruct.id X
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.sum.inrCompAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) :
        ((inrCompAssociator C D E).hom.app X).down.down = CategoryStruct.id X
        source
        🔸 coverage
        def CategoryTheory.sum.inlCompInlCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
        (Sum.inl_ C D).comp ((Sum.inl_ (C ⊕ D) E).comp (associator C D E)) ≅ Sum.inl_ C (D ⊕ E)

        Further characterizing the composition of the associator and the left inclusion.

        Instances For
          source
          📐 coverage
          @[simp]
          theorem CategoryTheory.sum.inlCompInlCompAssociator_inv_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) :
          ((inlCompInlCompAssociator C D E).inv.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inl X)).down (CategoryStruct.id (Sum.inl X)).down
          source
          📐 coverage
          @[simp]
          theorem CategoryTheory.sum.inlCompInlCompAssociator_hom_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) :
          ((inlCompInlCompAssociator C D E).hom.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inl X)).down (CategoryStruct.id (Sum.inl X)).down
          source
          🔸 coverage
          def CategoryTheory.sum.inrCompInlCompAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
          (Sum.inr_ C D).comp ((Sum.inl_ (C ⊕ D) E).comp (associator C D E)) ≅ (Sum.inl_ D E).comp (Sum.inr_ C (D ⊕ E))

          Further characterizing the composition of the associator and the left inclusion.

          Instances For
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.sum.inrCompInlCompAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) :
            ((inrCompInlCompAssociator C D E).hom.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.sum.inrCompInlCompAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) :
            ((inrCompInlCompAssociator C D E).inv.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down (CategoryStruct.id (Sum.inr (Sum.inl X))).down.down
            source
            🔸 coverage
            def CategoryTheory.sum.inverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
            Functor (C ⊕ D ⊕ E) ((C ⊕ D) ⊕ E)

            The inverse associator functor C ⊕ (D ⊕ E) ⥤ (C ⊕ D) ⊕ E for sums of categories.

            Instances For
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.sum.inverseAssociator_obj_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) :
              (inverseAssociator C D E).obj (Sum.inl X) = Sum.inl (Sum.inl X)
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.sum.inverseAssociator_obj_inr_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) :
              (inverseAssociator C D E).obj (Sum.inr (Sum.inl X)) = Sum.inl (Sum.inr X)
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.sum.inverseAssociator_obj_inr_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) :
              (inverseAssociator C D E).obj (Sum.inr (Sum.inr X)) = Sum.inr X
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.sum.inverseAssociator_map_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : C} (f : X ⟶ Y) :
              (inverseAssociator C D E).map ((Sum.inl_ C (D ⊕ E)).map f) = (Sum.inl_ (C ⊕ D) E).map ((Sum.inl_ C D).map f)
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.sum.inverseAssociator_map_inr_inl (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : D} (f : X ⟶ Y) :
              (inverseAssociator C D E).map ((Sum.inr_ C (D ⊕ E)).map ((Sum.inl_ D E).map f)) = (Sum.inl_ (C ⊕ D) E).map ((Sum.inr_ C D).map f)
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.sum.inverseAssociator_map_inr_inr (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {X Y : E} (f : X ⟶ Y) :
              (inverseAssociator C D E).map ((Sum.inr_ C (D ⊕ E)).map ((Sum.inr_ D E).map f)) = (Sum.inr_ (C ⊕ D) E).map f
              source
              🔸 coverage
              def CategoryTheory.sum.inlCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
              (Sum.inl_ C (D ⊕ E)).comp (inverseAssociator C D E) ≅ (Sum.inl_ C D).comp (Sum.inl_ (C ⊕ D) E)

              Characterizing the composition of the inverse of the associator and the left inclusion.

              Instances For
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.sum.inlCompInverseAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) :
                ((inlCompInverseAssociator C D E).hom.app X).down.down = CategoryStruct.id X
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.sum.inlCompInverseAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : C) :
                ((inlCompInverseAssociator C D E).inv.app X).down.down = CategoryStruct.id X
                source
                🔸 coverage
                def CategoryTheory.sum.inrCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                (Sum.inr_ C (D ⊕ E)).comp (inverseAssociator C D E) ≅ ((Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)).sum' (Sum.inr_ (C ⊕ D) E)

                Characterizing the composition of the inverse of the associator and the right inclusion.

                Instances For
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.sum.inrCompInverseAssociator_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D ⊕ E) :
                  (inrCompInverseAssociator C D E).hom.app X = CategoryStruct.id ((((Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)).sum' (Sum.inr_ (C ⊕ D) E)).obj X)
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.sum.inrCompInverseAssociator_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D ⊕ E) :
                  (inrCompInverseAssociator C D E).inv.app X = CategoryStruct.id ((((Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)).sum' (Sum.inr_ (C ⊕ D) E)).obj X)
                  source
                  🔸 coverage
                  def CategoryTheory.sum.inlCompInrCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                  (Sum.inl_ D E).comp ((Sum.inr_ C (D ⊕ E)).comp (inverseAssociator C D E)) ≅ (Sum.inr_ C D).comp (Sum.inl_ (C ⊕ D) E)

                  Further characterizing the composition of the inverse of the associator and the right inclusion.

                  Instances For
                    source
                    📐 coverage
                    @[simp]
                    theorem CategoryTheory.sum.inlCompInrCompInverseAssociator_inv_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) :
                    ((inlCompInrCompInverseAssociator C D E).inv.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down
                    source
                    📐 coverage
                    @[simp]
                    theorem CategoryTheory.sum.inlCompInrCompInverseAssociator_hom_app_down_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : D) :
                    ((inlCompInrCompInverseAssociator C D E).hom.app X).down.down = CategoryStruct.comp (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down (CategoryStruct.id (Sum.inl (Sum.inr X))).down.down
                    source
                    🔸 coverage
                    def CategoryTheory.sum.inrCompInrCompInverseAssociator (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                    (Sum.inr_ D E).comp ((Sum.inr_ C (D ⊕ E)).comp (inverseAssociator C D E)) ≅ Sum.inr_ (C ⊕ D) E

                    Further characterizing the composition of the inverse of the associator and the right inclusion.

                    Instances For
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.sum.inrCompInrCompInverseAssociator_hom_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) :
                      ((inrCompInrCompInverseAssociator C D E).hom.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inr X)).down (CategoryStruct.id (Sum.inr X)).down
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.sum.inrCompInrCompInverseAssociator_inv_app_down (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (X : E) :
                      ((inrCompInrCompInverseAssociator C D E).inv.app X).down = CategoryStruct.comp (CategoryStruct.id (Sum.inr X)).down (CategoryStruct.id (Sum.inr X)).down
                      source
                      🔸 coverage
                      def CategoryTheory.sum.associativity (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                      (C ⊕ D) ⊕ E ≌ C ⊕ D ⊕ E

                      The equivalence of categories expressing associativity of sums of categories.

                      Instances For
                        source
                        📐 coverage
                        @[simp]
                        theorem CategoryTheory.sum.associativity_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                        (associativity C D E).functor = associator C D E
                        source
                        📐 coverage
                        @[simp]
                        theorem CategoryTheory.sum.associativity_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                        (associativity C D E).inverse = inverseAssociator C D E
                        source
                        📐 coverage
                        instance CategoryTheory.sum.associatorIsEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                        (associator C D E).IsEquivalence
                        source
                        📐 coverage
                        instance CategoryTheory.sum.inverseAssociatorIsEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :
                        (inverseAssociator C D E).IsEquivalence