Documentation

Mathlib.CategoryTheory.GradedObject.Monoidal

The monoidal category structures on graded objects #

Assuming that C is a monoidal category and that I is an additive monoid, we introduce a partially defined tensor product on the category GradedObject I C: given X₁ and X₂ two objects in GradedObject I C, we define GradedObject.Monoidal.tensorObj X₁ X₂ under the assumption HasTensor X₁ X₂ that the coproduct of X₁ i ⊗ X₂ j for i + j = n exists for any n : I.

Under suitable assumptions about the existence of coproducts and the preservation of certain coproducts by the tensor products in C, we obtain a monoidal category structure on GradedObject I C. In particular, if C has finite coproducts to which the tensor product commutes, we obtain a monoidal category structure on GradedObject ℕ C.

@[reducible, inline]

The tensor product of two graded objects X₁ and X₂ exists if for any n, the coproduct of the objects X₁ i ⊗ X₂ j for i + j = n exists.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem CategoryTheory.GradedObject.hasTensor_of_iso {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e₁ : X₁ Y₁) (e₂ : X₂ Y₂) [X₁.HasTensor X₂] :
    Y₁.HasTensor Y₂
    @[reducible, inline]

    The tensor product of two graded objects.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def CategoryTheory.GradedObject.Monoidal.ιTensorObj {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) :

      The inclusion of a summand in a tensor product of two graded objects.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def CategoryTheory.GradedObject.Monoidal.tensorObjDesc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k(CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) A)) :

        Constructor for morphisms from a tensor product of two graded objects.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k(CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) A)) (i₁ i₂ : I) (hi : i₁ + i₂ = k) :
          @[simp]
          theorem CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k(CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) A)) (i₁ i₂ : I) (hi : i₁ + i₂ = k) {Z : C} (h : A Z) :
          noncomputable def CategoryTheory.GradedObject.Monoidal.tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ X₂) (g : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] :

          The morphism tensorObj X₁ Y₁ ⟶ tensorObj X₂ Y₂ induced by morphisms of graded objects f : X₁ ⟶ X₂ and g : Y₁ ⟶ Y₂.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.GradedObject.Monoidal.ι_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ X₂) (g : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) :
            @[simp]
            theorem CategoryTheory.GradedObject.Monoidal.ι_tensorHom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ X₂) (g : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) {Z : C} (h✝ : CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y₂ i₁₂ Z) :
            @[reducible, inline]

            The morphism tensorObj X Y₁ ⟶ tensorObj X Y₂ induced by a morphism of graded objects φ : Y₁ ⟶ Y₂.

            Equations
            Instances For
              @[reducible, inline]

              The morphism tensorObj X₁ Y ⟶ tensorObj X₂ Y induced by a morphism of graded objects φ : X₁ ⟶ X₂.

              Equations
              Instances For
                theorem CategoryTheory.GradedObject.Monoidal.tensor_comp {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₃.HasTensor Y₃] :
                noncomputable def CategoryTheory.GradedObject.Monoidal.tensorIso {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e : X₁ X₂) (e' : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] :

                The isomorphism tensorObj X₁ Y₁ ≅ tensorObj X₂ Y₂ induced by isomorphisms of graded objects e : X₁ ≅ X₂ and e' : Y₁ ≅ Y₂.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.GradedObject.Monoidal.tensorIso_inv {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e : X₁ X₂) (e' : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i : I) :
                  @[simp]
                  theorem CategoryTheory.GradedObject.Monoidal.tensorIso_hom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (e : X₁ X₂) (e' : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i : I) :

                  This is the addition map I × I × I → I for an additive monoid I.

                  Equations
                  Instances For
                    @[reducible]

                    Auxiliary definition for associator.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible]

                      Auxiliary definition for associator.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible]
                        def CategoryTheory.GradedObject.Monoidal.triangleIndexData (I : Type u) [AddMonoid I] :
                        CategoryTheory.GradedObject.TriangleIndexData CategoryTheory.GradedObject.Monoidal.r₁₂₃ fun (x : I × I) => match x with | (i₁, i₃) => i₁ + i₃

                        Auxiliary definition for associator.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[reducible, inline]

                          Given three graded objects X₁, X₂, X₃ in GradedObject I C, this is the assumption that for all i₁₂ : I and i₃ : I, the tensor product functor - ⊗ X₃ i₃ commutes with the coproduct of the objects X₁ i₁ ⊗ X₂ i₂ such that i₁ + i₂ = i₁₂.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[reducible, inline]

                            Given three graded objects X₁, X₂, X₃ in GradedObject I C, this is the assumption that for all i₁ : I and i₂₃ : I, the tensor product functor X₁ i₁ ⊗ - commutes with the coproduct of the objects X₂ i₂ ⊗ X₃ i₃ such that i₂ + i₃ = i₂₃.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              The inclusion X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⟶ tensorObj X₁ (tensorObj X₂ X₃) j when i₁ + i₂ + i₃ = j.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) :
                                @[simp]
                                theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
                                theorem CategoryTheory.GradedObject.Monoidal.tensorObj₃_ext {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ : CategoryTheory.GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] {j : I} {A : C} (f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j A) [H : X₁.HasGoodTensorTensor₂₃ X₂ X₃] (h : ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) g) :
                                f = g

                                The inclusion X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⟶ tensorObj (tensorObj X₁ X₂) X₃ j when i₁ + i₂ + i₃ = j.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) :
                                  @[simp]
                                  theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [Y₁.HasTensor Y₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃] (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
                                  theorem CategoryTheory.GradedObject.Monoidal.tensorObj₃'_ext {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] {j : I} {A : C} (f g : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j A) [H : X₁.HasGoodTensor₁₂Tensor X₂ X₃] (h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) g) :
                                  f = g
                                  noncomputable def CategoryTheory.GradedObject.Monoidal.associator {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] :

                                  The associator isomorphism for graded objects.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
                                    @[simp]
                                    theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h✝ : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j Z) :
                                    @[simp]
                                    theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
                                    @[simp]
                                    theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h✝ : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j Z) :
                                    theorem CategoryTheory.GradedObject.Monoidal.associator_naturality {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [Y₁.HasTensor Y₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃] [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃] [Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃] :
                                    @[reducible, inline]

                                    Given Z : C and three graded objects X₁, X₂ and X₃ in GradedObject I C, this typeclass expresses that functor Z ⊗ _ commutes with the coproduct of the objects X₁ i₁ ⊗ (X₂ i₂ ⊗ X₃ i₃) such that i₁ + i₂ + i₃ = j for a certain j. See lemma left_tensor_tensorObj₃_ext.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      The inclusion X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⊗ X₄ i₄ ⟶ tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j when i₁ + i₂ + i₃ + i₄ = j.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₄_eq {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C) [X₃.HasTensor X₄] [X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))] (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j) (i₂₃₄ : I) (hi : i₂ + i₃ + i₄ = i₂₃₄) :
                                        @[reducible, inline]

                                        Given four graded objects, this is the condition HasLeftTensor₃ObjExt (X₁ i₁) X₂ X₃ X₄ i₂₃₄ for all indices i₁ and i₂₃₄, see the lemma tensorObj₄_ext.

                                        Equations
                                        Instances For
                                          theorem CategoryTheory.GradedObject.Monoidal.tensorObj₄_ext {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C} [X₃.HasTensor X₄] [X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))] {j : I} {A : C} (f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)) j A) [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [H : X₁.HasTensor₄ObjExt X₂ X₃ X₄] (h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h) g) :
                                          f = g
                                          theorem CategoryTheory.GradedObject.Monoidal.pentagon_inv {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [X₃.HasTensor X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄] [X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [(CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor X₄] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄] [X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄] [X₂.HasGoodTensor₁₂Tensor X₃ X₄] [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄] [X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasTensor₄ObjExt X₂ X₃ X₄] :
                                          theorem CategoryTheory.GradedObject.Monoidal.pentagon_inv_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [X₃.HasTensor X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄] [X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [(CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor X₄] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄] [X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄] [X₂.HasGoodTensor₁₂Tensor X₃ X₄] [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄] [X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasTensor₄ObjExt X₂ X₃ X₄] {Z : CategoryTheory.GradedObject I C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃) X₄ Z) :
                                          theorem CategoryTheory.GradedObject.Monoidal.pentagon {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [X₃.HasTensor X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄] [X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [(CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor X₄] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄] [X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄] [X₂.HasGoodTensor₁₂Tensor X₃ X₄] [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄] [X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] [X₁.HasTensor₄ObjExt X₂ X₃ X₄] :

                                          The unit of the tensor product on graded objects is (single₀ I).obj (𝟙_ C).

                                          Equations
                                          Instances For

                                            The canonical isomorphism tensorUnit 0 ≅ 𝟙_ C

                                            Equations
                                            Instances For

                                              The left unitor isomorphism for graded objects.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                The right unitor isomorphism for graded objects.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  theorem CategoryTheory.GradedObject.Monoidal.triangle {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] (X₁ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ CategoryTheory.GradedObject.Monoidal.tensorUnit).HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X₃)] [X₁.HasGoodTensor₁₂Tensor CategoryTheory.GradedObject.Monoidal.tensorUnit X₃] [X₁.HasGoodTensorTensor₂₃ CategoryTheory.GradedObject.Monoidal.tensorUnit X₃] :
                                                  noncomputable instance CategoryTheory.GradedObject.monoidalCategory {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [DecidableEq I] [CategoryTheory.Limits.HasInitial C] [∀ (X₁ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] [∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] :
                                                  Equations

                                                  The monoidal category structure on GradedObject ℕ C can be inferred from the assumptions [HasFiniteCoproducts C], [∀ (X : C), PreservesFiniteCoproducts ((curriedTensor C).obj X)] and [∀ (X : C), PreservesFiniteCoproducts ((curriedTensor C).flip.obj X)]. This requires importing Mathlib.CategoryTheory.Limits.Preserves.Finite.