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.

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasTensor {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) : 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.

Equations

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

@[reducible, inline]

noncomputable abbrev 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₂] : CategoryTheory.GradedObject I C

The tensor product of two graded objects.

Equations

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

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₁₂) : CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ 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.

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₁ : CategoryTheory.GradedObject I C} {X₂ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] {A : C} {j : I} (f : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A) (g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A) (h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) g) : f = g

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)) : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ k ⟶ A

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

Equations

• CategoryTheory.GradedObject.Monoidal.tensorObjDesc f = CategoryTheory.GradedObject.mapBifunctorMapObjDesc f

@[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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) h) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ hi) h

@[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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi) (CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) = f i₁ i₂ hi

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₁ : 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₂] : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ Y₁ ⟶ CategoryTheory.GradedObject.Monoidal.tensorObj X₂ 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.

@[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₁ : 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₁₂) {Z : C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y₂ i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f i₁) (g i₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h✝) h)

@[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₁₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f i₁) (g i₂)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)

@[reducible, inline]

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

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

Equations

• CategoryTheory.GradedObject.Monoidal.whiskerLeft X φ = CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X) φ

@[reducible, inline]

noncomputable abbrev CategoryTheory.GradedObject.Monoidal.whiskerRight {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₁ ⟶ X₂) (Y : CategoryTheory.GradedObject I C) [X₁.HasTensor Y] [X₂.HasTensor Y] : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ Y ⟶ CategoryTheory.GradedObject.Monoidal.tensorObj X₂ Y

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

Equations

• CategoryTheory.GradedObject.Monoidal.whiskerRight φ Y = CategoryTheory.GradedObject.Monoidal.tensorHom φ (CategoryTheory.CategoryStruct.id Y)

@[simp]

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

theorem CategoryTheory.GradedObject.Monoidal.tensor_comp_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} {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {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₃] {Z : CategoryTheory.GradedObject I C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj X₃ Y₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂) h)

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₁ : 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} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₃.HasTensor Y₃] : CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁) (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂)

theorem CategoryTheory.GradedObject.Monoidal.tensorHom_def {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₂] [X₂.HasTensor Y₁] : CategoryTheory.GradedObject.Monoidal.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerRight f Y₁) (CategoryTheory.GradedObject.Monoidal.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.

Equations

• CategoryTheory.GradedObject.Monoidal.r₁₂₃ x = match x with | (i, j, k) => i + j + k

@[reducible]

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

Auxiliary definition for associator.

Equations

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

@[reducible]

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

Auxiliary definition for associator.

Equations

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

@[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.

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor {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) : Type (max (max (max u u_1) u_2) u)

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.

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ {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) : Type (max (max (max u u_1) u_2) u)

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.

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₁ : CategoryTheory.GradedObject I C) (X₂ : CategoryTheory.GradedObject I C) (X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [X₂.HasTensor X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ ≅ CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)

The associator isomorphism for graded objects.

Equations

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

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₃ : 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) : CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (CategoryTheory.MonoidalCategory.tensorObj (X₂ i₂) (X₃ i₃)) ⟶ CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j

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.

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq_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₃] [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₂₃) {Z : C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (X₁ i₁) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) i₁ i₂₃ j ⋯) h)

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₂₃) : CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (X₁ i₁) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h')) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) i₁ i₂₃ j ⋯)

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₃ : 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) : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂)) (X₃ i₃) ⟶ CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j

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.

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_eq_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₃] (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) {Z : C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯) h)

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₁₂) : CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom_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₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {Y₃ : CategoryTheory.GradedObject I C} [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f₁ i₁) (CategoryTheory.MonoidalCategory.tensorHom (f₂ i₂) (f₃ i₃))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h✝) h)

@[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₁ : 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₃)] {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {Y₃ : CategoryTheory.GradedObject I C} [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f₁ i₁) (CategoryTheory.MonoidalCategory.tensorHom (f₂ i₂) (f₃ i₃))) (CategoryTheory.GradedObject.Monoidal.ι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} [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₃] {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {Y₃ : CategoryTheory.GradedObject I C} [Y₁.HasTensor Y₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂) Y₃ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃ j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom (f₁ i₁) (f₂ i₂)) (f₃ i₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h✝) h)

@[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₁ : 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₃] {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {Y₃ : CategoryTheory.GradedObject I C} [Y₁.HasTensor Y₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ : I) (i₂ : I) (i₃ : I) (j : I) (h : i₁ + i₂ + i₃ = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃ j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom (f₁ i₁) (f₂ i₂)) (f₃ i₃)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)

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₁ : 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₃)] {j : I} {A : C} (f : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ A) (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

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₁ : 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₃] {j : I} {A : C} (f : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ A) (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

@[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₂] [X₂.HasTensor X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj 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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) h)

@[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₂] [X₂.HasTensor X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj 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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom (CategoryTheory.GradedObject.Monoidal.ι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} [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 X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj 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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ι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} [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 X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj 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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)

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} [X₁.HasTensor X₂] [X₂.HasTensor X₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] {Y₁ : CategoryTheory.GradedObject I C} {Y₂ : CategoryTheory.GradedObject I C} {Y₃ : CategoryTheory.GradedObject I C} [Y₁.HasTensor Y₂] [Y₂.HasTensor Y₃] [(CategoryTheory.GradedObject.Monoidal.tensorObj 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₃] : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃) (CategoryTheory.GradedObject.Monoidal.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃))