Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.associator_naturality

∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C}
  [inst_3 : X₁.HasTensor X₂] [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_5 : X₂.HasTensor X₃] [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : Y₁.HasTensor Y₂] [inst_8 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃]
  [inst_9 : Y₂.HasTensor Y₃] [inst_10 : Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)]
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) [inst_11 : X₁.HasGoodTensor₁₂Tensor X₂ X₃]
  [inst_12 : X₁.HasGoodTensorTensor₂₃ X₂ X₃] [inst_13 : Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃]
  [inst_14 : 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₃))

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

0 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃CategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃