Theorems · Theorem · category theory

Bimod.Hom.left_act_hom_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp M.actLeft (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.hom)
      (CategoryTheory.CategoryStruct.comp N.actLeft h)

Defined in

Mathlib.CategoryTheory.Monoidal.Bimod

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory