Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.pentagon_inv

∀ {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₃ X₄ : CategoryTheory.GradedObject I C)
  [inst_3 : X₁.HasTensor X₂] [inst_4 : X₂.HasTensor X₃] [inst_5 : X₃.HasTensor X₄]
  [inst_6 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_7 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_8 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄]
  [inst_9 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_10 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor
      X₄]
  [inst_11 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor
      X₄]
  [inst_12 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)]
  [inst_13 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  [inst_14 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_15 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_16 : X₁.HasGoodTensorTensor₂₃ X₂ X₃]
  [inst_17 : X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_18 : X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_19 : X₂.HasGoodTensor₁₂Tensor X₃ X₄] [inst_20 : X₂.HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_21 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄]
  [inst_22 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_23 : X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_24 : 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

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

1 results in Mathlib

Foundations

Depth 45 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.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasTensorCategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃CategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃CategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃CategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃CategoryTheory.GradedObject.HasGoodTensor₁₂TensorCategoryTheory.GradedObject.HasGoodTensorTensor₂₃CategoryTheory.GradedObject.HasTensor₄ObjExt