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]

abbrev CategoryTheory.GradedObject.HasTensor {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ : GradedObject I C) : Prop

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.

theorem CategoryTheory.GradedObject.hasTensor_of_iso {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (e₁ : X₁ ≅ Y₁) (e₂ : X₂ ≅ Y₂) [X₁.HasTensor X₂] : Y₁.HasTensor Y₂

@[reducible, inline]

noncomputable abbrev CategoryTheory.GradedObject.Monoidal.tensorObj {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ : GradedObject I C) [X₁.HasTensor X₂] : GradedObject I C

The tensor product of two graded objects.

noncomputable def CategoryTheory.GradedObject.Monoidal.ιTensorObj {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ : GradedObject I C) [X₁.HasTensor X₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) : MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ tensorObj X₁ X₂ i₁₂

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

theorem CategoryTheory.GradedObject.Monoidal.tensorObj_ext {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ : GradedObject I C} [X₁.HasTensor X₂] {A : C} {j : I} (f g : tensorObj X₁ X₂ j ⟶ A) (h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), CategoryStruct.comp (ιTensorObj X₁ X₂ i₁ i₂ j hi) f = CategoryStruct.comp (ιTensorObj X₁ X₂ i₁ i₂ j hi) g) : f = g

theorem CategoryTheory.GradedObject.Monoidal.tensorObj_ext_iff {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ : GradedObject I C} [X₁.HasTensor X₂] {A : C} {j : I} {f g : tensorObj X₁ X₂ j ⟶ A} : f = g ↔ ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), CategoryStruct.comp (ιTensorObj X₁ X₂ i₁ i₂ j hi) f = CategoryStruct.comp (ιTensorObj X₁ X₂ i₁ i₂ j hi) g

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorObjDesc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ : GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k → (MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) : tensorObj X₁ X₂ k ⟶ A

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

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ : GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k → (MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) (i₁ i₂ : I) (hi : i₁ + i₂ = k) : CategoryStruct.comp (ιTensorObj X₁ X₂ i₁ i₂ k hi) (tensorObjDesc f) = f i₁ i₂ hi

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ : GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k → (MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) (i₁ i₂ : I) (hi : i₁ + i₂ = k) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (ιTensorObj X₁ X₂ i₁ i₂ k hi) (CategoryStruct.comp (tensorObjDesc f) h) = CategoryStruct.comp (f i₁ i₂ hi) h

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] : tensorObj X₁ Y₁ ⟶ tensorObj X₂ Y₂

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

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ι_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) : CategoryStruct.comp (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (tensorHom f g i₁₂) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (f i₁) (g i₂)) (ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ι_tensorHom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : 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✝ : tensorObj X₂ Y₂ i₁₂ ⟶ Z) : CategoryStruct.comp (ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (CategoryStruct.comp (tensorHom f g i₁₂) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (f i₁) (g i₂)) (CategoryStruct.comp (ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h) h✝)

@[reducible, inline]

noncomputable abbrev CategoryTheory.GradedObject.Monoidal.whiskerLeft {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X : GradedObject I C) {Y₁ Y₂ : GradedObject I C} (φ : Y₁ ⟶ Y₂) [X.HasTensor Y₁] [X.HasTensor Y₂] : tensorObj X Y₁ ⟶ tensorObj X Y₂

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.GradedObject.Monoidal.whiskerRight {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ : GradedObject I C} (φ : X₁ ⟶ X₂) (Y : GradedObject I C) [X₁.HasTensor Y] [X₂.HasTensor Y] : tensorObj X₁ Y ⟶ tensorObj X₂ Y

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

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.id_tensorHom_id {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X Y : GradedObject I C) [X.HasTensor Y] : tensorHom (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (tensorObj X Y)

theorem CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₃.HasTensor Y₃] : CategoryStruct.comp (tensorHom f₁ g₁) (tensorHom f₂ g₂) = tensorHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)

theorem CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₃.HasTensor Y₃] {Z : GradedObject I C} (h : tensorObj X₃ Y₃ ⟶ Z) : CategoryStruct.comp (tensorHom f₁ g₁) (CategoryStruct.comp (tensorHom f₂ g₂) h) = CategoryStruct.comp (tensorHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)) h

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorIso {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] : tensorObj X₁ Y₁ ≅ tensorObj X₂ Y₂

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

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.tensorIso_hom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i : I) : (tensorIso e e').hom i = tensorHom e.hom e'.hom i

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.tensorIso_inv {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (e : X₁ ≅ X₂) (e' : Y₁ ≅ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i : I) : (tensorIso e e').inv i = tensorHom e.inv e'.inv i

theorem CategoryTheory.GradedObject.Monoidal.tensorHom_def {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₂.HasTensor Y₁] : tensorHom f g = CategoryStruct.comp (whiskerRight f Y₁) (whiskerLeft X₂ g)

def CategoryTheory.GradedObject.Monoidal.r₁₂₃ {I : Type u} [AddMonoid I] : I × I × I → I

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

@[reducible]

def CategoryTheory.GradedObject.Monoidal.ρ₁₂ {I : Type u} [AddMonoid I] : BifunctorComp₁₂IndexData r₁₂₃

Auxiliary definition for associator.

@[reducible]

def CategoryTheory.GradedObject.Monoidal.ρ₂₃ {I : Type u} [AddMonoid I] : BifunctorComp₂₃IndexData r₁₂₃

Auxiliary definition for associator.

@[reducible]

def CategoryTheory.GradedObject.Monoidal.triangleIndexData (I : Type u) [AddMonoid I] : TriangleIndexData r₁₂₃ fun (x : I × I) => match x with | (i₁, i₃) => i₁ + i₃

Auxiliary definition for associator.

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) : Prop

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

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) : Prop

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

noncomputable def CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : MonoidalCategoryStruct.tensorObj (X₁ i₁) (MonoidalCategoryStruct.tensorObj (X₂ i₂) (X₃ i₃)) ⟶ tensorObj X₁ (tensorObj X₂ X₃) j

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

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) : ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X₁ i₁) (ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h')) (ιTensorObj X₁ (tensorObj X₂ X₃) i₁ i₂₃ j ⋯)

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) {Z : C} (h✝ : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ Z) : CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X₁ i₁) (ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h')) (CategoryStruct.comp (ιTensorObj X₁ (tensorObj X₂ X₃) i₁ i₂₃ j ⋯) h✝)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [Y₂.HasTensor Y₃] [Y₁.HasTensor (tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (tensorHom f₁ (tensorHom f₂ f₃) j) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (f₁ i₁) (MonoidalCategoryStruct.tensorHom (f₂ i₂) (f₃ i₃))) (ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [Y₂.HasTensor Y₃] [Y₁.HasTensor (tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h✝ : tensorObj Y₁ (tensorObj Y₂ Y₃) j ⟶ Z) : CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryStruct.comp (tensorHom f₁ (tensorHom f₂ f₃) j) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (f₁ i₁) (MonoidalCategoryStruct.tensorHom (f₂ i₂) (f₃ i₃))) (CategoryStruct.comp (ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h) h✝)

theorem CategoryTheory.GradedObject.Monoidal.tensorObj₃_ext {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ : GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] {j : I} {A : C} (f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A) [H : X₁.HasGoodTensorTensor₂₃ X₂ X₃] (h : ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j), CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) f = CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) g) : f = g

noncomputable def CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂)) (X₃ i₃) ⟶ tensorObj (tensorObj X₁ X₂) X₃ j

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

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) : ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃)) (ιTensorObj (tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯)

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) {Z : C} (h✝ : tensorObj (tensorObj X₁ X₂) X₃ j ⟶ Z) : CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃)) (CategoryStruct.comp (ιTensorObj (tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯) h✝)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [Y₁.HasTensor Y₂] [(tensorObj Y₁ Y₂).HasTensor Y₃] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) (tensorHom (tensorHom f₁ f₂) f₃ j) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom (f₁ i₁) (f₂ i₂)) (f₃ i₃)) (ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_tensorHom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [Y₁.HasTensor Y₂] [(tensorObj Y₁ Y₂).HasTensor Y₃] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h✝ : tensorObj (tensorObj Y₁ Y₂) Y₃ j ⟶ Z) : CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃ j) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom (f₁ i₁) (f₂ i₂)) (f₃ i₃)) (CategoryStruct.comp (ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h) h✝)

theorem CategoryTheory.GradedObject.Monoidal.tensorObj₃'_ext {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ : GradedObject I C} [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] {j : I} {A : C} (f g : tensorObj (tensorObj X₁ X₂) X₃ j ⟶ A) [H : X₁.HasGoodTensor₁₂Tensor X₂ X₃] (h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryStruct.comp (ι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} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] : tensorObj (tensorObj X₁ X₂) X₃ ≅ tensorObj X₁ (tensorObj X₂ X₃)

The associator isomorphism for graded objects.

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) ((associator X₁ X₂ X₃).hom j) = CategoryStruct.comp (MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (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✝ : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ Z) : CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryStruct.comp ((associator X₁ X₂ X₃).hom j) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom (CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((associator X₁ X₂ X₃).inv j) = CategoryStruct.comp (MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ : GradedObject I C) [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (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✝ : tensorObj (tensorObj X₁ X₂) X₃ j ⟶ Z) : CategoryStruct.comp (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryStruct.comp ((associator X₁ X₂ X₃).inv j) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv (CategoryStruct.comp (ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) h✝)

theorem CategoryTheory.GradedObject.Monoidal.associator_naturality {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} [X₁.HasTensor X₂] [(tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [Y₁.HasTensor Y₂] [(tensorObj Y₁ Y₂).HasTensor Y₃] [Y₂.HasTensor Y₃] [Y₁.HasTensor (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₃] : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasLeftTensor₃ObjExt {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (Z : C) (X₁ X₂ X₃ : GradedObject I C) (j : I) : Prop

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.

theorem CategoryTheory.GradedObject.Monoidal.left_tensor_tensorObj₃_ext {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ : GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] {j : I} {A : C} (Z : C) (f g : MonoidalCategoryStruct.tensorObj Z (tensorObj X₁ (tensorObj X₂ X₃) j) ⟶ A) [H : X₁.HasGoodTensorTensor₂₃ X₂ X₃] [hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j] (h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Z (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)) f = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Z (ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)) g) : f = g

noncomputable def CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ X₄ : GradedObject I C) [X₃.HasTensor X₄] [X₂.HasTensor (tensorObj X₃ X₄)] [X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))] (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j) : MonoidalCategoryStruct.tensorObj (X₁ i₁) (MonoidalCategoryStruct.tensorObj (X₂ i₂) (MonoidalCategoryStruct.tensorObj (X₃ i₃) (X₄ i₄))) ⟶ tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j

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

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₄_eq {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ X₄ : GradedObject I C) [X₃.HasTensor X₄] [X₂.HasTensor (tensorObj X₃ X₄)] [X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))] (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j) (i₂₃₄ : I) (hi : i₂ + i₃ + i₄ = i₂₃₄) : ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X₁ i₁) (ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi)) (ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j ⋯)

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasTensor₄ObjExt {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ X₄ : GradedObject I C) : Prop

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.

theorem CategoryTheory.GradedObject.Monoidal.tensorObj₄_ext {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {X₁ X₂ X₃ X₄ : GradedObject I C} [X₃.HasTensor X₄] [X₂.HasTensor (tensorObj X₃ X₄)] [X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))] {j : I} {A : C} (f g : tensorObj X₁ (tensorObj X₂ (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), CategoryStruct.comp (ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h) f = CategoryStruct.comp (ι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} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ X₄ : GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [X₃.HasTensor X₄] [(tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [(tensorObj X₂ X₃).HasTensor X₄] [X₂.HasTensor (tensorObj X₃ X₄)] [(tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄] [(tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄] [X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)] [X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))] [(tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄] [X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄] [X₂.HasGoodTensor₁₂Tensor X₃ X₄] [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [(tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄] [(tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄] [X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)] [X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)] [X₁.HasTensor₄ObjExt X₂ X₃ X₄] : CategoryStruct.comp (tensorHom (CategoryStruct.id X₁) (associator X₂ X₃ X₄).inv) (CategoryStruct.comp (associator X₁ (tensorObj X₂ X₃) X₄).inv (tensorHom (associator X₁ X₂ X₃).inv (CategoryStruct.id X₄))) = CategoryStruct.comp (associator X₁ X₂ (tensorObj X₃ X₄)).inv (associator (tensorObj X₁ X₂) X₃ X₄).inv

theorem CategoryTheory.GradedObject.Monoidal.pentagon_inv_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ X₄ : GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [X₃.HasTensor X₄] [(tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [(tensorObj X₂ X₃).HasTensor X₄] [X₂.HasTensor (tensorObj X₃ X₄)] [(tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄] [(tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄] [X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)] [X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))] [(tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄] [X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄] [X₂.HasGoodTensor₁₂Tensor X₃ X₄] [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [(tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄] [(tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄] [X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)] [X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)] [X₁.HasTensor₄ObjExt X₂ X₃ X₄] {Z : GradedObject I C} (h : tensorObj (tensorObj (tensorObj X₁ X₂) X₃) X₄ ⟶ Z) : CategoryStruct.comp (tensorHom (CategoryStruct.id X₁) (associator X₂ X₃ X₄).inv) (CategoryStruct.comp (associator X₁ (tensorObj X₂ X₃) X₄).inv (CategoryStruct.comp (tensorHom (associator X₁ X₂ X₃).inv (CategoryStruct.id X₄)) h)) = CategoryStruct.comp (associator X₁ X₂ (tensorObj X₃ X₄)).inv (CategoryStruct.comp (associator (tensorObj X₁ X₂) X₃ X₄).inv h)

theorem CategoryTheory.GradedObject.Monoidal.pentagon {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (X₁ X₂ X₃ X₄ : GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [X₃.HasTensor X₄] [(tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (tensorObj X₂ X₃)] [(tensorObj X₂ X₃).HasTensor X₄] [X₂.HasTensor (tensorObj X₃ X₄)] [(tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄] [(tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄] [X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)] [X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))] [(tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄] [X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄] [X₂.HasGoodTensor₁₂Tensor X₃ X₄] [X₂.HasGoodTensorTensor₂₃ X₃ X₄] [(tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄] [(tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄] [X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)] [X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)] [X₁.HasTensor₄ObjExt X₂ X₃ X₄] : CategoryStruct.comp (tensorHom (associator X₁ X₂ X₃).hom (CategoryStruct.id X₄)) (CategoryStruct.comp (associator X₁ (tensorObj X₂ X₃) X₄).hom (tensorHom (CategoryStruct.id X₁) (associator X₂ X₃ X₄).hom)) = CategoryStruct.comp (associator (tensorObj X₁ X₂) X₃ X₄).hom (associator X₁ X₂ (tensorObj X₃ X₄)).hom

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorUnit {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] : GradedObject I C

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

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorUnit₀ {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] : tensorUnit 0 ≅ MonoidalCategoryStruct.tensorUnit C

The canonical isomorphism tensorUnit 0 ≅ 𝟙_ C

noncomputable def CategoryTheory.GradedObject.Monoidal.isInitialTensorUnitApply {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] (i : I) (hi : i ≠ 0) : Limits.IsInitial (tensorUnit i)

tensorUnit i is an initial object when i ≠ 0.

instance CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] (X : GradedObject I C) : tensorUnit.HasTensor X

instance CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] (X : GradedObject I C) : (((mapBifunctor (MonoidalCategory.curriedTensor C) I I).obj ((single₀ I).obj (MonoidalCategoryStruct.tensorUnit C))).obj X).HasMap fun (x : I × I) => match x with | (i₁, i₂) => i₁ + i₂

noncomputable def CategoryTheory.GradedObject.Monoidal.leftUnitor {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] (X : GradedObject I C) : tensorObj tensorUnit X ≅ X

The left unitor isomorphism for graded objects.

theorem CategoryTheory.GradedObject.Monoidal.leftUnitor_inv_apply {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] (X : GradedObject I C) (i : I) : (leftUnitor X).inv i = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (X i)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight tensorUnit₀.inv (X i)) (ιTensorObj tensorUnit X 0 i i ⋯))

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.leftUnitor_naturality {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] {X X' : GradedObject I C} (φ : X ⟶ X') : CategoryStruct.comp (tensorHom (CategoryStruct.id tensorUnit) φ) (leftUnitor X').hom = CategoryStruct.comp (leftUnitor X).hom φ

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.leftUnitor_naturality_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] {X X' : GradedObject I C} (φ : X ⟶ X') {Z : GradedObject I C} (h : X' ⟶ Z) : CategoryStruct.comp (tensorHom (CategoryStruct.id tensorUnit) φ) (CategoryStruct.comp (leftUnitor X').hom h) = CategoryStruct.comp (leftUnitor X).hom (CategoryStruct.comp φ h)

instance CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit_1 {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] (X : GradedObject I C) : X.HasTensor tensorUnit

instance CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1 {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] (X : GradedObject I C) : (((mapBifunctor (MonoidalCategory.curriedTensor C) I I).obj X).obj ((single₀ I).obj (MonoidalCategoryStruct.tensorUnit C))).HasMap fun (x : I × I) => match x with | (i₁, i₂) => i₁ + i₂

noncomputable def CategoryTheory.GradedObject.Monoidal.rightUnitor {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] (X : GradedObject I C) : tensorObj X tensorUnit ≅ X

The right unitor isomorphism for graded objects.

theorem CategoryTheory.GradedObject.Monoidal.rightUnitor_inv_apply {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] (X : GradedObject I C) (i : I) : (rightUnitor X).inv i = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (X i)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (X i) tensorUnit₀.inv) (ιTensorObj X tensorUnit i 0 i ⋯))

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] {X X' : GradedObject I C} (φ : X ⟶ X') : CategoryStruct.comp (tensorHom φ (CategoryStruct.id tensorUnit)) (rightUnitor X').hom = CategoryStruct.comp (rightUnitor X).hom φ

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] {X X' : GradedObject I C} (φ : X ⟶ X') {Z : GradedObject I C} (h : X' ⟶ Z) : CategoryStruct.comp (tensorHom φ (CategoryStruct.id tensorUnit)) (CategoryStruct.comp (rightUnitor X').hom h) = CategoryStruct.comp (rightUnitor X).hom (CategoryStruct.comp φ h)

theorem CategoryTheory.GradedObject.Monoidal.triangle {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] (X₁ X₃ : GradedObject I C) [X₁.HasTensor X₃] [(tensorObj X₁ tensorUnit).HasTensor X₃] [X₁.HasTensor (tensorObj tensorUnit X₃)] [X₁.HasGoodTensor₁₂Tensor tensorUnit X₃] [X₁.HasGoodTensorTensor₂₃ tensorUnit X₃] : CategoryStruct.comp (associator X₁ tensorUnit X₃).hom (tensorHom (CategoryStruct.id X₁) (leftUnitor X₃).hom) = tensorHom (rightUnitor X₁).hom (CategoryStruct.id X₃)

noncomputable instance CategoryTheory.GradedObject.monoidalCategory {I : Type u} [AddMonoid I] {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂] [∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] [∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [DecidableEq I] [Limits.HasInitial C] [∀ (X₁ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).obj X₁)] [∀ (X₂ : C), Limits.PreservesColimit (Functor.empty C) ((MonoidalCategory.curriedTensor C).flip.obj X₂)] [∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] : MonoidalCategory (GradedObject I C)

instance CategoryTheory.GradedObject.instFiniteElemProdNatPreimageHAddFstSndSingletonSet (n : ℕ) : Finite ↑((fun (i : ℕ × ℕ) => i.1 + i.2) ⁻¹' {n})

instance CategoryTheory.GradedObject.instFiniteElemProdNatSetOfEqHAddFstSnd (n : ℕ) : Finite ↑{i : ℕ × ℕ × ℕ | i.1 + i.2.1 + i.2.2 = n}

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