Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.hexagon_forward

∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y Z : CategoryTheory.GradedObject I C)
  [inst_3 : CategoryTheory.BraidedCategory C] [inst_4 : X.HasTensor Y] [inst_5 : Y.HasTensor X] [inst_6 : Y.HasTensor Z]
  [inst_7 : Z.HasTensor X] [inst_8 : X.HasTensor Z]
  [inst_9 : (CategoryTheory.GradedObject.Monoidal.tensorObj X Y).HasTensor Z]
  [inst_10 : X.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)]
  [inst_11 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z).HasTensor X]
  [inst_12 : Y.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Z X)]
  [inst_13 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y X).HasTensor Z]
  [inst_14 : Y.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X Z)] [inst_15 : X.HasGoodTensor₁₂Tensor Y Z]
  [inst_16 : X.HasGoodTensorTensor₂₃ Y Z] [inst_17 : Y.HasGoodTensor₁₂Tensor Z X]
  [inst_18 : Y.HasGoodTensorTensor₂₃ Z X] [inst_19 : Y.HasGoodTensor₁₂Tensor X Z]
  [inst_20 : Y.HasGoodTensorTensor₂₃ X Z],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.braiding X (CategoryTheory.GradedObject.Monoidal.tensorObj Y Z)).hom
        (CategoryTheory.GradedObject.Monoidal.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.whiskerRight (CategoryTheory.GradedObject.Monoidal.braiding X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator Y X Z).hom
        (CategoryTheory.GradedObject.Monoidal.whiskerLeft Y (CategoryTheory.GradedObject.Monoidal.braiding X Z).hom))

Defined in

Mathlib.CategoryTheory.GradedObject.Braiding

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategoryCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.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₂₃CategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃