# Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

# 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 Module R in Algebra.Category.ModuleCat.Monoidal.Closed.

If you're happy using the bundled Module 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} [] (M : ) (N : ) :

(implementation) tensor product of R-modules

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

(implementation) tensor product of morphisms R-modules

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

(implementation) left whiskering for R-modules

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

(implementation) right whiskering for R-modules

Instances For
theorem ModuleCat.MonoidalCategory.tensor_id {R : Type u} [] (M : ) (N : ) :
theorem ModuleCat.MonoidalCategory.tensor_comp {R : Type u} [] {X₁ : } {Y₁ : } {Z₁ : } {X₂ : } {Y₂ : } {Z₂ : } (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :
def ModuleCat.MonoidalCategory.associator {R : Type u} [] (M : ) (N : ) (K : ) :

(implementation) the associator for R-modules

Instances For

The associator_naturality and pentagon lemmas below are very slow to elaborate.

We give them some help by expressing the lemmas first non-categorically, then using convert _aux using 1 to have the elaborator work as little as possible.

theorem ModuleCat.MonoidalCategory.associator_naturality {R : Type u} [] {X₁ : } {X₂ : } {X₃ : } {Y₁ : } {Y₂ : } {Y₃ : } (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
=
theorem ModuleCat.MonoidalCategory.pentagon {R : Type u} [] (W : ) (X : ) (Y : ) (Z : ) :

(implementation) the left unitor for R-modules

Instances For
theorem ModuleCat.MonoidalCategory.leftUnitor_naturality {R : Type u} [] {M : } {N : } (f : M N) :

(implementation) the right unitor for R-modules

Instances For
theorem ModuleCat.MonoidalCategory.rightUnitor_naturality {R : Type u} [] {M : } {N : } (f : M N) :
theorem ModuleCat.MonoidalCategory.triangle {R : Type u} [] (M : ) (N : ) :

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

@[simp]
theorem ModuleCat.MonoidalCategory.hom_apply {R : Type u} [] {K : } {L : } {M : } {N : } (f : K L) (g : M N) (k : K) (m : M) :
↑() (k ⊗ₜ[R] m) = f k ⊗ₜ[R] g m
@[simp]
theorem ModuleCat.MonoidalCategory.leftUnitor_hom_apply {R : Type u} [] {M : } (r : R) (m : M) :
(r ⊗ₜ[R] m) = r m
@[simp]
theorem ModuleCat.MonoidalCategory.leftUnitor_inv_apply {R : Type u} [] {M : } (m : M) :
= 1 ⊗ₜ[R] m
@[simp]
theorem ModuleCat.MonoidalCategory.rightUnitor_hom_apply {R : Type u} [] {M : } (m : M) (r : R) :
(m ⊗ₜ[R] r) = r m
@[simp]
theorem ModuleCat.MonoidalCategory.rightUnitor_inv_apply {R : Type u} [] {M : } (m : M) :
= m ⊗ₜ[R] 1
@[simp]
theorem ModuleCat.MonoidalCategory.associator_hom_apply {R : Type u} [] {M : } {N : } {K : } (m : M) (n : N) (k : K) :
().hom ((m ⊗ₜ[R] n) ⊗ₜ[R] k) = m ⊗ₜ[R] n ⊗ₜ[R] k
@[simp]
theorem ModuleCat.MonoidalCategory.associator_inv_apply {R : Type u} [] {M : } {N : } {K : } (m : M) (n : N) (k : K) :
().inv (m ⊗ₜ[R] n ⊗ₜ[R] k) = (m ⊗ₜ[R] n) ⊗ₜ[R] k