@[reducible, inline]

abbrev CategoryTheory.Bimodule {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : Mon C) : Type (max u v)

An (A,B)-bimodule in a monoidal category C: an object equipped with commuting left A-action and right B-action.

@[reducible, inline]

abbrev CategoryTheory.Bimodule.obj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : Mon C} (M : Bimodule A B) : C

The underlying object of an (A,B)-bimodule.

@[reducible, inline]

abbrev CategoryTheory.Bimodule.leftAction {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : Mon C} (M : Bimodule A B) : MonoidalCategoryStruct.tensorObj A.X M.X ⟶ M.X

The left A-action morphism A ⊗ M → M of an (A,B)-bimodule.

@[reducible, inline]

abbrev CategoryTheory.Bimodule.rightAction {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : Mon C} (M : Bimodule A B) : MonoidalCategoryStruct.tensorObj M.X B.X ⟶ M.X

The right B-action morphism M ⊗ B → M of an (A,B)-bimodule.

theorem CategoryTheory.Bimodule.actions_commute {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : Mon C} (M : Bimodule A B) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight M.actLeft B.X) M.actRight = CategoryStruct.comp (MonoidalCategoryStruct.associator A.X M.X B.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A.X M.actRight) M.actLeft)

The middle-associativity (bimodule compatibility) axiom: the left and right actions on a bimodule commute up to the associator.