The balanced tensor product of modules over a commutative monoid

Let A be a commutative monoid object in a braided monoidal category C with coequalizers, such that tensoring on either side preserves (universe-0 small) colimits, in particular these coequalizers. The balanced tensor product M ⊗_A N of two left A-modules is the coequalizer of the two actions of A on M ⊗ A ⊗ N: the right action m ⊗ a ↦ a • m of A on M, obtained through the braiding, and the left action on N. The scalars act on M ⊗_A N through M. With unit the regular module A, this makes Mod C A a monoidal category.

For the commutative sphere monoid in symmetric sequences this is the smash product X ∧ Y of symmetric spectra, the coequalizer of X ⊗ S ⊗ Y ⇉ X ⊗ Y.

The construction reuses Mathlib's tensor product of bimodules Bimod.tensorBimod, with the associator and unitors of Mathlib's bicategory Bimod.monBicategory of monoids and bimodules. A module over a commutative monoid is a bimodule through Mod.toBimod. The bimodule tensor product of two such bimodules is again of this form (Bimod.tensorBimod_actRight_eq), so the monoidal structure Bimod.monoidalCategory of the endomorphism category Bimod R R is transported to Mod C A along the fully faithful functor Mod.toBimod by Mathlib's Monoidal.induced.

Main definitions

• Mod.monoidalCategory: the monoidal category of modules over a commutative monoid object, under the balanced tensor product.
• Mod.tensorπ M N : M.X ⊗ N.X ⟶ (M ⊗ N).X: the quotient map onto the balanced tensor product, and Mod.tensorDesc, its universal property.

Main statements

• Mod.tensorπ_whiskerLeft_hom, Mod.tensorπ_whiskerRight_hom, Mod.tensorπ_associator_hom_hom, Mod.tensorπ_associator_inv_hom, Mod.tensorπ_leftUnitor_hom_hom and Mod.tensorπ_rightUnitor_hom_hom: the monoidal structure on representatives in M.X ⊗ N.X.
• The instance (Mod.toBimod (A := A)).Monoidal: Mod.toBimod is a monoidal functor, with structure maps Mod.toBimod_μ, Mod.toBimod_δ, Mod.toBimod_ε and Mod.toBimod_η.

References

• M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 2.2.

noncomputable def CategoryTheory.Mod.tensorObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : Mod C A

The balanced tensor product M ⊗_A N of modules over a commutative monoid object: the tensor product of the associated bimodules, with its left action.

noncomputable def CategoryTheory.Mod.toBimodTensorObjIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : MonoidalCategoryStruct.tensorObj (toBimod.obj M) (toBimod.obj N) ≅ toBimod.obj (M.tensorObj N)

The bimodule associated with M ⊗_A N is the tensor product of the bimodules associated with M and N. The comparison is the identity on the common carrier.

@[instance_reducible]

noncomputable instance CategoryTheory.Mod.monoidalCategoryStruct {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] : MonoidalCategoryStruct (Mod C A)

The balanced tensor product, with the monoidal data of bimodules conjugated by toBimodTensorObjIso.

noncomputable def CategoryTheory.Mod.inducingFunctorData {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] : Monoidal.InducingFunctorData toBimod

The data inducing the monoidal structure of Mod C A from that of bimodules along toBimod.

@[instance_reducible]

noncomputable instance CategoryTheory.Mod.monoidalCategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] : MonoidalCategory (Mod C A)

Modules over a commutative monoid object form a monoidal category under the balanced tensor product, with unit the regular module.

@[instance_reducible]

noncomputable instance CategoryTheory.Mod.instMonoidalBimodMkToBimod {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] : toBimod.Monoidal

Regarding modules over a commutative monoid object as bimodules is a monoidal functor.

@[simp]

theorem CategoryTheory.Mod.toBimod_μ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : Functor.LaxMonoidal.μ toBimod M N = (M.toBimodTensorObjIso N).hom

The tensorator of the monoidal functor toBimod is the comparison toBimodTensorObjIso.

@[simp]

theorem CategoryTheory.Mod.toBimod_δ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : Functor.OplaxMonoidal.δ toBimod M N = (M.toBimodTensorObjIso N).inv

The inverse tensorator of toBimod is the inverse of toBimodTensorObjIso.

@[simp]

theorem CategoryTheory.Mod.toBimod_ε {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] : Functor.LaxMonoidal.ε toBimod = toBimodRegularIso.inv

The unit map of the monoidal functor toBimod is the inverse of toBimodRegularIso.

@[simp]

theorem CategoryTheory.Mod.toBimod_η {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] : Functor.OplaxMonoidal.η toBimod = toBimodRegularIso.hom

The counit map of the monoidal functor toBimod is toBimodRegularIso.

noncomputable def CategoryTheory.Mod.tensorπ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ (MonoidalCategoryStruct.tensorObj M N).X

The quotient map M ⊗ N ⟶ M ⊗_A N onto the balanced tensor product.

theorem CategoryTheory.Mod.tensorπ_condition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) (M.tensorπ N) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) (M.tensorπ N))

The quotient map onto M ⊗_A N identifies the action of A on M with that on N.

theorem CategoryTheory.Mod.tensorπ_condition_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) {Z : C} (h : (MonoidalCategoryStruct.tensorObj M N).X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) (CategoryStruct.comp (M.tensorπ N) h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) (CategoryStruct.comp (M.tensorπ N) h))

The quotient map onto M ⊗_A N identifies the action of A on M with that on N.

theorem CategoryTheory.Mod.smul_whiskerRight_tensorπ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ModObj.smul N.X) (M.tensorπ N) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (β_ A M.X).hom N.X) (CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) (M.tensorπ N)))

In M ⊗_A N, a scalar acting on M may be moved, through the braiding, to act on N.

theorem CategoryTheory.Mod.smul_whiskerRight_tensorπ_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) {Z : C} (h : (MonoidalCategoryStruct.tensorObj M N).X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ModObj.smul N.X) (CategoryStruct.comp (M.tensorπ N) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (β_ A M.X).hom N.X) (CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) (CategoryStruct.comp (M.tensorπ N) h)))

In M ⊗_A N, a scalar acting on M may be moved, through the braiding, to act on N.

instance CategoryTheory.Mod.instEpiTensorπ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : Epi (M.tensorπ N)

instance CategoryTheory.Mod.instEpiWhiskerRightTensorπ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) (X : C) : Epi (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) X)

Tensoring on the right preserves the coequalizer defining M ⊗_A N, so the whiskered quotient map is still an epimorphism.

instance CategoryTheory.Mod.instEpiWhiskerLeftTensorπ {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) (X : C) : Epi (MonoidalCategoryStruct.whiskerLeft X (M.tensorπ N))

Tensoring on the left preserves the coequalizer defining M ⊗_A N, so the whiskered quotient map is still an epimorphism.

theorem CategoryTheory.Mod.tensor_hom_ext {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} {f g : (MonoidalCategoryStruct.tensorObj M N).X ⟶ Z} (h : CategoryStruct.comp (M.tensorπ N) f = CategoryStruct.comp (M.tensorπ N) g) : f = g

Morphisms out of M ⊗_A N are determined by their composites with the quotient map.

theorem CategoryTheory.Mod.tensor_hom_ext_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} {f g : (MonoidalCategoryStruct.tensorObj M N).X ⟶ Z} : f = g ↔ CategoryStruct.comp (M.tensorπ N) f = CategoryStruct.comp (M.tensorπ N) g

noncomputable def CategoryTheory.Mod.tensorDesc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) : (MonoidalCategoryStruct.tensorObj M N).X ⟶ Z

A morphism out of M ⊗ N identifying the actions of A on M and on N factors through the balanced tensor product.

@[simp]

theorem CategoryTheory.Mod.tensorπ_tensorDesc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) : CategoryStruct.comp (M.tensorπ N) (tensorDesc f hf) = f

The factorization through the balanced tensor product restricts to the given morphism.

@[simp]

theorem CategoryTheory.Mod.tensorπ_tensorDesc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (M.tensorπ N) (CategoryStruct.comp (tensorDesc f hf) h) = CategoryStruct.comp f h

The factorization through the balanced tensor product restricts to the given morphism.

@[simp]

theorem CategoryTheory.Mod.whiskerLeft_tensorπ_tensorDesc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (M.tensorπ N)) (MonoidalCategoryStruct.whiskerLeft X (tensorDesc f hf)) = MonoidalCategoryStruct.whiskerLeft X f

The factorization through the balanced tensor product, whiskered on the left, restricts to the whiskered morphism.

@[simp]

theorem CategoryTheory.Mod.whiskerLeft_tensorπ_tensorDesc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) (X : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (M.tensorπ N)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (tensorDesc f hf)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) h

The factorization through the balanced tensor product, whiskered on the left, restricts to the whiskered morphism.

@[simp]

theorem CategoryTheory.Mod.tensorπ_tensorDesc_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) X) (MonoidalCategoryStruct.whiskerRight (tensorDesc f hf) X) = MonoidalCategoryStruct.whiskerRight f X

The factorization through the balanced tensor product, whiskered on the right, restricts to the whiskered morphism.

@[simp]

theorem CategoryTheory.Mod.tensorπ_tensorDesc_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M N : Mod C A} {Z : C} (f : MonoidalCategoryStruct.tensorObj M.X N.X ⟶ Z) (hf : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) N.X) f = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) f)) (X : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (tensorDesc f hf) X) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f X) h

The factorization through the balanced tensor product, whiskered on the right, restricts to the whiskered morphism.

@[simp]

theorem CategoryTheory.Mod.whiskerLeft_tensorπ_smul {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A (M.tensorπ N)) ModObj.smul = CategoryStruct.comp (MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ModObj.smul N.X) (M.tensorπ N))

The scalars act on M ⊗_A N through M.

@[simp]

theorem CategoryTheory.Mod.whiskerLeft_tensorπ_smul_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) {Z : C} (h : (MonoidalCategoryStruct.tensorObj M N).X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A (M.tensorπ N)) (CategoryStruct.comp ModObj.smul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator A M.X N.X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ModObj.smul N.X) (CategoryStruct.comp (M.tensorπ N) h))

The scalars act on M ⊗_A N through M.

theorem CategoryTheory.Mod.tensorπ_toBimodTensorObjIso_inv_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : CategoryStruct.comp (M.tensorπ N) (M.toBimodTensorObjIso N).inv.hom = Limits.coequalizer.π (MonoidalCategoryStruct.whiskerRight (toBimod.obj M).actRight (toBimod.obj N).X) (CategoryStruct.comp (MonoidalCategoryStruct.associator (toBimod.obj M).X { X := A, mon := inst✝ }.X (toBimod.obj N).X).hom (MonoidalCategoryStruct.whiskerLeft (toBimod.obj M).X (toBimod.obj N).actLeft))

The comparison toBimodTensorObjIso carries the quotient map onto M ⊗_A N to the quotient map onto the tensor product of bimodules.

theorem CategoryTheory.Mod.π_toBimodTensorObjIso_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N : Mod C A) : CategoryStruct.comp (Limits.coequalizer.π (MonoidalCategoryStruct.whiskerRight (toBimod.obj M).actRight (toBimod.obj N).X) (CategoryStruct.comp (MonoidalCategoryStruct.associator (toBimod.obj M).X { X := A, mon := inst✝ }.X (toBimod.obj N).X).hom (MonoidalCategoryStruct.whiskerLeft (toBimod.obj M).X (toBimod.obj N).actLeft))) (M.toBimodTensorObjIso N).hom.hom = M.tensorπ N

The comparison toBimodTensorObjIso carries the quotient map onto the tensor product of bimodules to the quotient map onto M ⊗_A N.

@[simp]

theorem CategoryTheory.Mod.tensorπ_whiskerLeft_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) {N N' : Mod C A} (g : N ⟶ N') : CategoryStruct.comp (M.tensorπ N) (MonoidalCategoryStruct.whiskerLeft M g).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X g.hom) (M.tensorπ N')

Whiskering g : N ⟶ N' on the left by M acts on representatives as M.X ◁ g.hom.

@[simp]

theorem CategoryTheory.Mod.tensorπ_whiskerLeft_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) {N N' : Mod C A} (g : N ⟶ N') {Z : C} (h : (MonoidalCategoryStruct.tensorObj M N').X ⟶ Z) : CategoryStruct.comp (M.tensorπ N) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M g).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X g.hom) (CategoryStruct.comp (M.tensorπ N') h)

Whiskering g : N ⟶ N' on the left by M acts on representatives as M.X ◁ g.hom.

@[simp]

theorem CategoryTheory.Mod.tensorπ_whiskerRight_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M M' : Mod C A} (f : M ⟶ M') (N : Mod C A) : CategoryStruct.comp (M.tensorπ N) (MonoidalCategoryStruct.whiskerRight f N).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f.hom N.X) (M'.tensorπ N)

Whiskering f : M ⟶ M' on the right by N acts on representatives as f.hom ▷ N.X.

@[simp]

theorem CategoryTheory.Mod.tensorπ_whiskerRight_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M M' : Mod C A} (f : M ⟶ M') (N : Mod C A) {Z : C} (h : (MonoidalCategoryStruct.tensorObj M' N).X ⟶ Z) : CategoryStruct.comp (M.tensorπ N) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f N).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f.hom N.X) (CategoryStruct.comp (M'.tensorπ N) h)

Whiskering f : M ⟶ M' on the right by N acts on representatives as f.hom ▷ N.X.

@[simp]

theorem CategoryTheory.Mod.tensorπ_tensorHom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M M' N N' : Mod C A} (f : M ⟶ M') (g : N ⟶ N') : CategoryStruct.comp (M.tensorπ N) (MonoidalCategoryStruct.tensorHom f g).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f.hom g.hom) (M'.tensorπ N')

The tensor product of f : M ⟶ M' and g : N ⟶ N' acts on representatives as f.hom ⊗ₘ g.hom.

@[simp]

theorem CategoryTheory.Mod.tensorπ_tensorHom_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] {M M' N N' : Mod C A} (f : M ⟶ M') (g : N ⟶ N') {Z : C} (h : (MonoidalCategoryStruct.tensorObj M' N').X ⟶ Z) : CategoryStruct.comp (M.tensorπ N) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f.hom g.hom) (CategoryStruct.comp (M'.tensorπ N') h)

The tensor product of f : M ⟶ M' and g : N ⟶ N' acts on representatives as f.hom ⊗ₘ g.hom.

theorem CategoryTheory.Mod.tensorπ_associator_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N P : Mod C A) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) P.X) (CategoryStruct.comp ((MonoidalCategoryStruct.tensorObj M N).tensorπ P) (MonoidalCategoryStruct.associator M N P).hom.hom) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X N.X P.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X (N.tensorπ P)) (M.tensorπ (MonoidalCategoryStruct.tensorObj N P)))

The associator of M ⊗_A N ⊗_A P acts on representatives in M.X ⊗ N.X ⊗ P.X as the associator of the underlying objects.

theorem CategoryTheory.Mod.tensorπ_associator_hom_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N P : Mod C A) {Z : C} (h : (MonoidalCategoryStruct.tensorObj M (MonoidalCategoryStruct.tensorObj N P)).X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) P.X) (CategoryStruct.comp ((MonoidalCategoryStruct.tensorObj M N).tensorπ P) (CategoryStruct.comp (MonoidalCategoryStruct.associator M N P).hom.hom h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X N.X P.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X (N.tensorπ P)) (CategoryStruct.comp (M.tensorπ (MonoidalCategoryStruct.tensorObj N P)) h))

The associator of M ⊗_A N ⊗_A P acts on representatives in M.X ⊗ N.X ⊗ P.X as the associator of the underlying objects.

theorem CategoryTheory.Mod.tensorπ_associator_inv_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N P : Mod C A) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X (N.tensorπ P)) (CategoryStruct.comp (M.tensorπ (MonoidalCategoryStruct.tensorObj N P)) (MonoidalCategoryStruct.associator M N P).inv.hom) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X N.X P.X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) P.X) ((MonoidalCategoryStruct.tensorObj M N).tensorπ P))

The inverse associator of M ⊗_A (N ⊗_A P) acts on representatives in M.X ⊗ N.X ⊗ P.X as the inverse associator of the underlying objects.

theorem CategoryTheory.Mod.tensorπ_associator_inv_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M N P : Mod C A) {Z : C} (h : (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj M N) P).X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X (N.tensorπ P)) (CategoryStruct.comp (M.tensorπ (MonoidalCategoryStruct.tensorObj N P)) (CategoryStruct.comp (MonoidalCategoryStruct.associator M N P).inv.hom h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X N.X P.X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (M.tensorπ N) P.X) (CategoryStruct.comp ((MonoidalCategoryStruct.tensorObj M N).tensorπ P) h))

The inverse associator of M ⊗_A (N ⊗_A P) acts on representatives in M.X ⊗ N.X ⊗ P.X as the inverse associator of the underlying objects.

@[simp]

theorem CategoryTheory.Mod.tensorπ_leftUnitor_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) : CategoryStruct.comp ((MonoidalCategoryStruct.tensorUnit (Mod C A)).tensorπ M) (MonoidalCategoryStruct.leftUnitor M).hom.hom = ModObj.smul

The left unitor of 𝟙_ ⊗_A M is induced by the action γ[A, M.X] of A on M.

@[simp]

theorem CategoryTheory.Mod.tensorπ_leftUnitor_hom_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) {Z : C} (h : M.X ⟶ Z) : CategoryStruct.comp ((MonoidalCategoryStruct.tensorUnit (Mod C A)).tensorπ M) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor M).hom.hom h) = CategoryStruct.comp ModObj.smul h

The left unitor of 𝟙_ ⊗_A M is induced by the action γ[A, M.X] of A on M.

@[simp]

theorem CategoryTheory.Mod.tensorπ_rightUnitor_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) : CategoryStruct.comp (M.tensorπ (MonoidalCategoryStruct.tensorUnit (Mod C A))) (MonoidalCategoryStruct.rightUnitor M).hom.hom = CategoryStruct.comp (β_ A M.X).inv ModObj.smul

The right unitor of M ⊗_A 𝟙_ is induced by the action of A on M precomposed with the inverse braiding.

@[simp]

theorem CategoryTheory.Mod.tensorπ_rightUnitor_hom_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] [Limits.HasCoequalizers C] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorLeft X)] [∀ (X : C), Limits.PreservesColimitsOfSize.{0, 0, v, v, u, u} (MonoidalCategory.tensorRight X)] {A : C} [MonObj A] [IsCommMonObj A] (M : Mod C A) {Z : C} (h : M.X ⟶ Z) : CategoryStruct.comp (M.tensorπ (MonoidalCategoryStruct.tensorUnit (Mod C A))) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor M).hom.hom h) = CategoryStruct.comp (CategoryStruct.comp (β_ A M.X).inv ModObj.smul) h

The right unitor of M ⊗_A 𝟙_ is induced by the action of A on M precomposed with the inverse braiding.