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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ 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.

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

@[reducible, inline]

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₁ 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₁ X₂ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] (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₁ X₂ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] {A : C} {j : I} (f 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₁ 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 {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] {A : C} {k : I} (f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) (i₁ i₂ : I) (hi : i₁ + i₂ = k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi) (CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) = f i₁ i₂ hi

@[simp]

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

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] : 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 {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] (i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) : 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)

@[simp]

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

@[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₁ 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₁ 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 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 {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₃.HasTensor Y₃] : 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.tensor_comp_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [X₁.HasTensor Y₁] [X₂.HasTensor Y₂] [X₃.HasTensor Y₃] {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)

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

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

Equations

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

@[simp]

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

@[simp]

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

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₁ X₂ Y₁ 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₁₂₃ (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₁ X₂ X₃ : CategoryTheory.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₁₂.

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₁ X₂ X₃ : CategoryTheory.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₂₃.

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₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : 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 {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) : 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 ⋯)

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

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : 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₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {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✝)

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

noncomputable def CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : 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 {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₁₂ : I) (h' : i₁ + i₂ = i₁₂) : 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 ⋯)

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

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_tensorHom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [Y₁.HasTensor Y₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : 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)

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

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

noncomputable def CategoryTheory.GradedObject.Monoidal.associator {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] : 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.

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_associator_hom {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : 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_hom_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h✝ : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ Z) : 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_inv {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) : 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)

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_associator_inv_assoc {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) {Z : C} (h✝ : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ Z) : 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✝)

theorem CategoryTheory.GradedObject.Monoidal.associator_naturality {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} [X₁.HasTensor X₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [X₂.HasTensor X₃] [X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] [Y₁.HasTensor Y₂] [(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃] [Y₂.HasTensor Y₃] [Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)] (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) [X₁.HasGoodTensor₁₂Tensor X₂ X₃] [X₁.HasGoodTensorTensor₂₃ X₂ X₃] [Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃] [Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃] : 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₃))

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasLeftTensor₃ObjExt {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (Z : C) (X₁ X₂ X₃ : CategoryTheory.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.

Equations

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

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

Equations

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

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

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasTensor₄ObjExt {I : Type u} [AddMonoid I] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C) : 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.

Equations

• X₁.HasTensor₄ObjExt X₂ X₃ X₄ = ∀ (i₁ i₂₃₄ : I), CategoryTheory.GradedObject.HasLeftTensor₃ObjExt (X₁ i₁) X₂ X₃ X₄ i₂₃₄

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

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

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

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

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorUnit {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] : CategoryTheory.GradedObject I C

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

Equations

• CategoryTheory.GradedObject.Monoidal.tensorUnit = (CategoryTheory.GradedObject.single₀ I).obj (𝟙_ C)

noncomputable def CategoryTheory.GradedObject.Monoidal.tensorUnit₀ {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] : CategoryTheory.GradedObject.Monoidal.tensorUnit 0 ≅ 𝟙_ C

The canonical isomorphism tensorUnit 0 ≅ 𝟙_ C

Equations

• CategoryTheory.GradedObject.Monoidal.tensorUnit₀ = CategoryTheory.GradedObject.singleObjApplyIso 0 (𝟙_ C)

noncomputable def CategoryTheory.GradedObject.Monoidal.isInitialTensorUnitApply {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] (i : I) (hi : i ≠ 0) : CategoryTheory.Limits.IsInitial (CategoryTheory.GradedObject.Monoidal.tensorUnit i)

tensorUnit i is an initial object when i ≠ 0.

Equations

• CategoryTheory.GradedObject.Monoidal.isInitialTensorUnitApply i hi = CategoryTheory.GradedObject.isInitialSingleObjApply 0 (𝟙_ C) i hi

instance CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit {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).flip.obj X₂)] (X : CategoryTheory.GradedObject I C) : CategoryTheory.GradedObject.Monoidal.tensorUnit.HasTensor X

instance CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit {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).flip.obj X₂)] (X : CategoryTheory.GradedObject I C) : (((CategoryTheory.GradedObject.mapBifunctor (CategoryTheory.MonoidalCategory.curriedTensor C) I I).obj ((CategoryTheory.GradedObject.single₀ I).obj (𝟙_ 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} [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).flip.obj X₂)] (X : CategoryTheory.GradedObject I C) : CategoryTheory.GradedObject.Monoidal.tensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X ≅ X

The left unitor isomorphism for graded objects.

Equations

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

theorem CategoryTheory.GradedObject.Monoidal.leftUnitor_inv_apply {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).flip.obj X₂)] (X : CategoryTheory.GradedObject I C) (i : I) : (CategoryTheory.GradedObject.Monoidal.leftUnitor X).inv i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (X i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv (X i)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X 0 i i ⋯))

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.leftUnitor_naturality {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).flip.obj X₂)] {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X') : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit) φ) (CategoryTheory.GradedObject.Monoidal.leftUnitor X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X).hom φ

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.leftUnitor_naturality_assoc {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).flip.obj X₂)] {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X') {Z : CategoryTheory.GradedObject I C} (h : X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit) φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp φ h)

instance CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit_1 {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 : CategoryTheory.GradedObject I C) : X.HasTensor CategoryTheory.GradedObject.Monoidal.tensorUnit

instance CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1 {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 : CategoryTheory.GradedObject I C) : (((CategoryTheory.GradedObject.mapBifunctor (CategoryTheory.MonoidalCategory.curriedTensor C) I I).obj X).obj ((CategoryTheory.GradedObject.single₀ I).obj (𝟙_ 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} [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 : CategoryTheory.GradedObject I C) : CategoryTheory.GradedObject.Monoidal.tensorObj X CategoryTheory.GradedObject.Monoidal.tensorUnit ≅ X

The right unitor isomorphism for graded objects.

Equations

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

theorem CategoryTheory.GradedObject.Monoidal.rightUnitor_inv_apply {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 : CategoryTheory.GradedObject I C) (i : I) : (CategoryTheory.GradedObject.Monoidal.rightUnitor X).inv i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (X i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (X i) CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X CategoryTheory.GradedObject.Monoidal.tensorUnit i 0 i ⋯))

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality {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 X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X') : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom φ (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit)) (CategoryTheory.GradedObject.Monoidal.rightUnitor X').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X).hom φ

@[simp]

theorem CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality_assoc {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 X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X') {Z : CategoryTheory.GradedObject I C} (h : X' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom φ (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp φ h)

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

Equations

• CategoryTheory.GradedObject.monoidalCategory = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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.