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
    @[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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] (i₁ : I) (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₁ : CategoryTheory.GradedObject I C} {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_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.GradedObject I C} {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₂ : I) (hi : i₁ + i₂ = k) {Z : C} (h : A Z) :
          @[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₁ : CategoryTheory.GradedObject I C} {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₂ : I) (hi : i₁ + i₂ = k) :

          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₁ : CategoryTheory.GradedObject I C} {X₂ : CategoryTheory.GradedObject I C} {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} (f : X₁ X₂) (g : Y₁ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i₁ : I) (i₂ : I) (i₁₂ : I) (h : i₁ + i₂ = i₁₂) :
            @[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

                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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) :
                              @[simp]

                              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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) :
                                @[simp]

                                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_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (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₂ : 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_hom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (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₂ : 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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (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₂ : 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) :
                                  @[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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (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₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) :
                                  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₁ : CategoryTheory.GradedObject I C} {X₂ : CategoryTheory.GradedObject I C} {X₃ : CategoryTheory.GradedObject I C} {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) (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) (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.pentagon_inv_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) (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_inv {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) (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 {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) (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₁ : CategoryTheory.GradedObject I C) (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
                                                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.