noncomputable def CategoryTheory.tensorOverAlgebra {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M N : C) (rmod : RightModObj A M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : C

Definition 2.9.22: the tensor product M ⊗_A N of a right A-module M and a left A-module N in a monoidal category, constructed as a coequalizer.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Definition_2_9_22 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M N : C) (rmod : RightModObj A M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : C

Definition 2.9.22: alias for the tensor product M ⊗_A N over an algebra in a monoidal category.

noncomputable def CategoryTheory.tensorOverAlgebra.π {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M N : C) (rmod : RightModObj A M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : MonoidalCategoryStruct.tensorObj M N ⟶ tensorOverAlgebra M N rmod actL

The canonical coequalizer projection M ⊗ N → M ⊗_A N realizing the tensor product over A.

theorem CategoryTheory.tensorOverAlgebra.condition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] [Limits.HasCoequalizers C] (M N : C) (rmod : RightModObj A M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight rmod.act N) (π M N rmod actL) = CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.associator M A N).hom (MonoidalCategoryStruct.whiskerLeft M actL)) (π M N rmod actL)

The coequalizer relation defining M ⊗_A N: the two ways of acting by A (on M from the right and on N from the left) become equal after composing with the projection.