Theorems · Theorem · category theory

SemimoduleCat.MonoidalCategory.pentagon

∀ {R : Type u} [inst : CommSemiring R] (W : SemimoduleCat R) (X : SemimoduleCat R) (Y : SemimoduleCat R)
  (Z : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.whiskerRight (SemimoduleCat.MonoidalCategory.associator W X Y).hom Z)
      (CategoryTheory.CategoryStruct.comp
        (SemimoduleCat.MonoidalCategory.associator W (SemimoduleCat.MonoidalCategory.tensorObj X Y) Z).hom
        (SemimoduleCat.MonoidalCategory.whiskerLeft W (SemimoduleCat.MonoidalCategory.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.associator (SemimoduleCat.MonoidalCategory.tensorObj W X) Y Z).hom
      (SemimoduleCat.MonoidalCategory.associator W X (SemimoduleCat.MonoidalCategory.tensorObj Y Z)).hom

Defined in: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 71 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Quiver.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CommSemiringstatement and proof · cited by 10,911
CategoryTheory.Iso.homstatement and proof · cited by 7,684
TensorProduct.tmulproof · cited by 1,182
SemimoduleCatstatement and proof · cited by 108
SemimoduleCat.carrierproof · cited by 87
SemimoduleCat.Hom.homproof · cited by 45
SemimoduleCat.hom_extproof · cited by 15
SemimoduleCat.MonoidalCategory.tensorObjstatement and proof · cited by 12
SemimoduleCat.MonoidalCategory.associatorstatement and proof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.