The symmetric monoidal category of modules over a commutative monoid

Let A be a commutative monoid object in a symmetric monoidal category C with coequalizers preserved by tensoring. The balanced tensor product M ⊗_A N of TauCeti's Mod.monoidalCategory is then symmetric: the symmetry M ⊗ N ≅ N ⊗ M of C descends to an isomorphism M ⊗_A N ≅ N ⊗_A M of A-modules, and these isomorphisms satisfy the hexagon identities and square to the identity. This makes Mod C A a symmetric monoidal category, so commutative monoids in it (Mathlib's IsCommMonObj and CommMon) make sense. For the commutative sphere monoid in symmetric sequences this is the symmetric monoidal structure on the smash product of symmetric spectra, whose commutative monoids are the commutative symmetric ring spectra.

The symmetry of C is used already for the braiding to be well defined on the quotient M ⊗_A N, not only for its symmetry: the balancing relation moves scalars between the factors through the inverse braiding, and in a merely braided category the braiding of the factors need not respect it.

Main definitions

• Mod.symmetricCategory: modules over a commutative monoid object in a symmetric monoidal category form a symmetric monoidal category under the balanced tensor product.

Main statements

• Mod.braiding_tensorπ_condition and Mod.smul_tensorDesc_braiding: the braiding of the underlying objects descends to an A-linear map M ⊗_A N ⟶ N ⊗_A M.
• Mod.tensorπ_braiding_hom_hom and Mod.tensorπ_braiding_inv_hom: the braiding of Mod C A on representatives in M.X ⊗ N.X.

References

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

theorem CategoryTheory.Mod.braiding_tensorπ_condition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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) (CategoryStruct.comp (β_ M.X N.X).hom (N.tensorπ M)) = CategoryStruct.comp (MonoidalCategoryStruct.associator M.X A N.X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M.X ModObj.smul) (CategoryStruct.comp (β_ M.X N.X).hom (N.tensorπ M)))

The braiding of the underlying objects, followed by the quotient map onto N ⊗_A M, identifies the actions of A on M and on N.

theorem CategoryTheory.Mod.smul_tensorDesc_braiding {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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 ModObj.smul (tensorDesc (CategoryStruct.comp (β_ M.X N.X).hom (N.tensorπ M)) ⋯) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A (tensorDesc (CategoryStruct.comp (β_ M.X N.X).hom (N.tensorπ M)) ⋯)) ModObj.smul

The morphism M ⊗_A N ⟶ N ⊗_A M induced by the braiding M ⊗ N ⟶ N ⊗ M of the underlying objects is A-linear: the scalars act on M ⊗_A N through M and on N ⊗_A M through N, and these agree on N ⊗_A M by the balancing relation.

@[instance_reducible]

noncomputable instance CategoryTheory.Mod.symmetricCategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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] : SymmetricCategory (Mod C A)

Modules over a commutative monoid object in a symmetric monoidal category form a symmetric monoidal category under the balanced tensor product, with braiding induced by that of C.

@[simp]

theorem CategoryTheory.Mod.tensorπ_braiding_hom_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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 N).hom.hom = CategoryStruct.comp (β_ M.X N.X).hom (N.tensorπ M)

On representatives, the braiding M ⊗_A N ≅ N ⊗_A M is the braiding of the underlying objects.

@[simp]

theorem CategoryTheory.Mod.tensorπ_braiding_hom_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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 N M).X ⟶ Z) : CategoryStruct.comp (M.tensorπ N) (CategoryStruct.comp (β_ M N).hom.hom h) = CategoryStruct.comp (β_ M.X N.X).hom (CategoryStruct.comp (N.tensorπ M) h)

On representatives, the braiding M ⊗_A N ≅ N ⊗_A M is the braiding of the underlying objects.

@[simp]

theorem CategoryTheory.Mod.tensorπ_braiding_inv_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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 (N.tensorπ M) (β_ M N).inv.hom = CategoryStruct.comp (β_ M.X N.X).inv (M.tensorπ N)

On representatives, the inverse braiding N ⊗_A M ≅ M ⊗_A N is the inverse braiding of the underlying objects.

@[simp]

theorem CategoryTheory.Mod.tensorπ_braiding_inv_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [SymmetricCategory 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 (N.tensorπ M) (CategoryStruct.comp (β_ M N).inv.hom h) = CategoryStruct.comp (β_ M.X N.X).inv (CategoryStruct.comp (M.tensorπ N) h)

On representatives, the inverse braiding N ⊗_A M ≅ M ⊗_A N is the inverse braiding of the underlying objects.