The monoidal category structure on R-modules

Mostly this uses existing machinery in LinearAlgebra.TensorProduct. We just need to provide a few small missing pieces to build the MonoidalCategory instance. The SymmetricCategory instance is in Algebra.Category.ModuleCat.Monoidal.Symmetric to reduce imports.

Note the universe level of the modules must be at least the universe level of the ring, so that we have a monoidal unit. For now, we simplify by insisting both universe levels are the same.

We construct the monoidal closed structure on ModuleCat R in Algebra.Category.ModuleCat.Monoidal.Closed.

If you're happy using the bundled ModuleCat R, it may be possible to mostly use this as an interface and not need to interact much with the implementation details.

def ModuleCat.MonoidalCategory.tensorObj {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) : ModuleCat R

(implementation) tensor product of R-modules

def ModuleCat.MonoidalCategory.tensorHom {R : Type u} [CommRing R] {M N : ModuleCat R} {M' N' : ModuleCat R} (f : M ⟶ N) (g : M' ⟶ N') : tensorObj M M' ⟶ tensorObj N N'

(implementation) tensor product of morphisms R-modules

def ModuleCat.MonoidalCategory.whiskerLeft {R : Type u} [CommRing R] (M : ModuleCat R) {N₁ N₂ : ModuleCat R} (f : N₁ ⟶ N₂) : tensorObj M N₁ ⟶ tensorObj M N₂

(implementation) left whiskering for R-modules

def ModuleCat.MonoidalCategory.whiskerRight {R : Type u} [CommRing R] {M₁ M₂ : ModuleCat R} (f : M₁ ⟶ M₂) (N : ModuleCat R) : tensorObj M₁ N ⟶ tensorObj M₂ N

(implementation) right whiskering for R-modules

theorem ModuleCat.MonoidalCategory.id_tensorHom_id {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) : tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (of R (TensorProduct R ↑M ↑N))

@[deprecated ModuleCat.MonoidalCategory.id_tensorHom_id (since := "2025-07-14")]

theorem ModuleCat.MonoidalCategory.tensor_id {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) : tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (of R (TensorProduct R ↑M ↑N))

Alias of ModuleCat.MonoidalCategory.id_tensorHom_id.

theorem ModuleCat.MonoidalCategory.tensor_comp {R : Type u} [CommRing R] {X₁ Y₁ Z₁ : ModuleCat R} {X₂ Y₂ Z₂ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂)

def ModuleCat.MonoidalCategory.associator {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) (K : ModuleCat R) : tensorObj (tensorObj M N) K ≅ tensorObj M (tensorObj N K)

(implementation) the associator for R-modules

def ModuleCat.MonoidalCategory.leftUnitor {R : Type u} [CommRing R] (M : ModuleCat R) : of R (TensorProduct R R ↑M) ≅ M

(implementation) the left unitor for R-modules

def ModuleCat.MonoidalCategory.rightUnitor {R : Type u} [CommRing R] (M : ModuleCat R) : of R (TensorProduct R (↑M) R) ≅ M

(implementation) the right unitor for R-modules

instance ModuleCat.MonoidalCategory.instMonoidalCategoryStruct {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategoryStruct (ModuleCat R)

theorem ModuleCat.MonoidalCategory.tensorUnit_isAddCommGroup {R : Type u} [CommRing R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)).isAddCommGroup = inst✝.toAddCommGroup

theorem ModuleCat.MonoidalCategory.whiskerLeft_def {R : Type u} [CommRing R] (M : ModuleCat R) {N₁ N₂ : ModuleCat R} (f : N₁ ⟶ N₂) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f = whiskerLeft M f

theorem ModuleCat.MonoidalCategory.tensorUnit_carrier {R : Type u} [CommRing R] : ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)) = R

theorem ModuleCat.MonoidalCategory.whiskerRight_def {R : Type u} [CommRing R] {X₁✝ X₂✝ : ModuleCat R} (f : X₁✝ ⟶ X₂✝) (N : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f N = whiskerRight f N

theorem ModuleCat.MonoidalCategory.leftUnitor_def {R : Type u} [CommRing R] (M : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.leftUnitor M = leftUnitor M

theorem ModuleCat.MonoidalCategory.rightUnitor_def {R : Type u} [CommRing R] (M : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.rightUnitor M = rightUnitor M

theorem ModuleCat.MonoidalCategory.tensorUnit_isModule {R : Type u} [CommRing R] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)).isModule = Semiring.toModule

theorem ModuleCat.MonoidalCategory.tensorObj_def {R : Type u} [CommRing R] (M N : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.tensorObj M N = tensorObj M N

theorem ModuleCat.MonoidalCategory.tensorHom_def {R : Type u} [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : ModuleCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ofHom (TensorProduct.map (Hom.hom f) (Hom.hom g))

theorem ModuleCat.MonoidalCategory.associator_def {R : Type u} [CommRing R] (M N K : ModuleCat R) : CategoryTheory.MonoidalCategoryStruct.associator M N K = associator M N K

theorem ModuleCat.MonoidalCategory.associator_naturality {R : Type u} [CommRing R] {X₁ : ModuleCat R} {X₂ : ModuleCat R} {X₃ : ModuleCat R} {Y₁ : ModuleCat R} {Y₂ : ModuleCat R} {Y₃ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))

theorem ModuleCat.MonoidalCategory.pentagon {R : Type u} [CommRing R] (W : ModuleCat R) (X : ModuleCat R) (Y : ModuleCat R) (Z : ModuleCat R) : CategoryTheory.CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryTheory.CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom

theorem ModuleCat.MonoidalCategory.leftUnitor_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (tensorHom (CategoryTheory.CategoryStruct.id (of R R)) f) (leftUnitor N).hom = CategoryTheory.CategoryStruct.comp (leftUnitor M).hom f

theorem ModuleCat.MonoidalCategory.rightUnitor_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (tensorHom f (CategoryTheory.CategoryStruct.id (of R R))) (rightUnitor N).hom = CategoryTheory.CategoryStruct.comp (rightUnitor M).hom f

theorem ModuleCat.MonoidalCategory.triangle {R : Type u} [CommRing R] (M N : ModuleCat R) : CategoryTheory.CategoryStruct.comp (associator M (of R R) N).hom (tensorHom (CategoryTheory.CategoryStruct.id M) (leftUnitor N).hom) = tensorHom (rightUnitor M).hom (CategoryTheory.CategoryStruct.id N)

instance ModuleCat.monoidalCategory {R : Type u} [CommRing R] : CategoryTheory.MonoidalCategory (ModuleCat R)

instance ModuleCat.instCommRingCarrierTensorUnit {R : Type u} [CommRing R] : CommRing ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))

Remind ourselves that the monoidal unit, being just R, is still a commutative ring.

@[simp]

theorem ModuleCat.MonoidalCategory.tensorHom_tmul {R : Type u} [CommRing R] {K L M N : ModuleCat R} (f : K ⟶ L) (g : M ⟶ N) (k : ↑K) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (k ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom f) k ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m

@[simp]

theorem ModuleCat.MonoidalCategory.whiskerLeft_apply {R : Type u} [CommRing R] (L : ModuleCat R) {M N : ModuleCat R} (f : M ⟶ N) (l : ↑L) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f)) (l ⊗ₜ[R] m) = l ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom f) m

@[simp]

theorem ModuleCat.MonoidalCategory.whiskerRight_apply {R : Type u} [CommRing R] {L M : ModuleCat R} (f : L ⟶ M) (N : ModuleCat R) (l : ↑L) (n : ↑N) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N)) (l ⊗ₜ[R] n) = (CategoryTheory.ConcreteCategory.hom f) l ⊗ₜ[R] n

@[simp]

theorem ModuleCat.MonoidalCategory.leftUnitor_hom_apply {R : Type u} [CommRing R] {M : ModuleCat R} (r : R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) (r ⊗ₜ[R] m) = r • m

@[simp]

theorem ModuleCat.MonoidalCategory.leftUnitor_inv_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv) m = 1 ⊗ₜ[R] m

@[simp]

theorem ModuleCat.MonoidalCategory.rightUnitor_hom_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) (r : R) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) (m ⊗ₜ[R] r) = r • m

@[simp]

theorem ModuleCat.MonoidalCategory.rightUnitor_inv_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv) m = m ⊗ₜ[R] 1

@[simp]

theorem ModuleCat.MonoidalCategory.associator_hom_apply {R : Type u} [CommRing R] {M N K : ModuleCat R} (m : ↑M) (n : ↑N) (k : ↑K) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom) (m ⊗ₜ[R] n ⊗ₜ[R] k) = m ⊗ₜ[R] (n ⊗ₜ[R] k)

@[simp]

theorem ModuleCat.MonoidalCategory.associator_inv_apply {R : Type u} [CommRing R] {M N K : ModuleCat R} (m : ↑M) (n : ↑N) (k : ↑K) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv) (m ⊗ₜ[R] (n ⊗ₜ[R] k)) = m ⊗ₜ[R] n ⊗ₜ[R] k

def ModuleCat.MonoidalCategory.tensorLift {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃) (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃

Construct for morphisms from the tensor product of two objects in ModuleCat.

@[simp]

theorem ModuleCat.MonoidalCategory.tensorLift_tmul {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃) (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n) (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n) (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂) (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) (m : ↑M₁) (n : ↑M₂) : (CategoryTheory.ConcreteCategory.hom (tensorLift f h₁ h₂ h₃ h₄)) (m ⊗ₜ[R] n) = f m n

theorem ModuleCat.MonoidalCategory.tensor_ext {R : Type u} [CommRing R] {M₁ M₂ M₃ : ModuleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃} (h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)) : f = g

theorem ModuleCat.MonoidalCategory.tensor_ext₃' {R : Type u} [CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂) M₃ ⟶ M₄} (h : ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃), (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)) : f = g

Extensionality lemma for morphisms from a module of the form (M₁ ⊗ M₂) ⊗ M₃.

theorem ModuleCat.MonoidalCategory.tensor_ext₃ {R : Type u} [CommRing R] {M₁ M₂ M₃ M₄ : ModuleCat R} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃) ⟶ M₄} (h : ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃), (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))) : f = g

Extensionality lemma for morphisms from a module of the form M₁ ⊗ (M₂ ⊗ M₃).

instance ModuleCat.instMonoidalPreadditive {R : Type u} [CommRing R] : CategoryTheory.MonoidalPreadditive (ModuleCat R)

instance ModuleCat.instMonoidalLinear {R : Type u} [CommRing R] : CategoryTheory.MonoidalLinear R (ModuleCat R)

@[simp]

theorem ModuleCat.ofHom₂_compr₂ {R : Type u} [CommRing R] {M N P Q : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) (g : ↑P →ₗ[R] ↑Q) : ofHom₂ (f.compr₂ g) = CategoryTheory.CategoryStruct.comp (ofHom₂ f) (ofHom (CategoryTheory.Linear.rightComp R N (ofHom g)))