Theorems · Theorem · category theory

Bimod.pentagon_bimod

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {V W X Y Z : CategoryTheory.Mon C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z),
  CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight (M.associatorBimod N P).hom Q)
      (CategoryTheory.CategoryStruct.comp (M.associatorBimod (N.tensorBimod P) Q).hom
        (M.whiskerLeft (N.associatorBimod P Q).hom)) =
    CategoryTheory.CategoryStruct.comp ((M.tensorBimod N).associatorBimod P Q).hom
      (M.associatorBimod N (P.tensorBimod Q)).hom

Defined in

Mathlib.CategoryTheory.Monoidal.Bimod

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Limits.HasCoequalizersCategoryTheory.Limits.PreservesColimitsOfSizeCategoryTheory.Limits.PreservesColimitsOfSize