mathlib documentation


The monoidal category structure on R-modules #

Mostly this uses existing machinery in linear_algebra.tensor_product. We just need to provide a few small missing pieces to build the monoidal_category instance. The symmetric_category instance is in algebra.category.Module.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.Module.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 Module.monoidal_category.tensor_obj {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :

(implementation) tensor product of R-modules


(implementation) tensor product of morphisms R-modules

theorem Module.monoidal_category.tensor_comp {R : Type u} [comm_ring R] {X₁ Y₁ Z₁ : Module R} {X₂ Y₂ Z₂ : Module R} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :

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 Module.monoidal_category.associator_naturality {R : Type u} [comm_ring R] {X₁ : Module R} {X₂ : Module R} {X₃ : Module R} {Y₁ : Module R} {Y₂ : Module R} {Y₃ : Module R} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :

(implementation) the left unitor for R-modules


(implementation) the right unitor for R-modules

@[protected, instance]

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

theorem Module.monoidal_category.hom_apply {R : Type u} [comm_ring R] {K L M N : Module R} (f : K L) (g : M N) (k : K) (m : M) :
(f g) (k ⊗ₜ[R] m) = f k ⊗ₜ[R] g m
theorem Module.monoidal_category.left_unitor_hom_apply {R : Type u} [comm_ring R] {M : Module R} (r : R) (m : M) :
((λ_ M).hom) (r ⊗ₜ[R] m) = r m
theorem Module.monoidal_category.left_unitor_inv_apply {R : Type u} [comm_ring R] {M : Module R} (m : M) :
((λ_ M).inv) m = 1 ⊗ₜ[R] m
theorem Module.monoidal_category.right_unitor_hom_apply {R : Type u} [comm_ring R] {M : Module R} (m : M) (r : R) :
((ρ_ M).hom) (m ⊗ₜ[R] r) = r m
theorem Module.monoidal_category.right_unitor_inv_apply {R : Type u} [comm_ring R] {M : Module R} (m : M) :
((ρ_ M).inv) m = m ⊗ₜ[R] 1
theorem Module.monoidal_category.associator_hom_apply {R : Type u} [comm_ring R] {M N K : Module R} (m : M) (n : N) (k : K) :
((α_ M N K).hom) (m ⊗ₜ[R] n ⊗ₜ[R] k) = m ⊗ₜ[R] (n ⊗ₜ[R] k)
theorem Module.monoidal_category.associator_inv_apply {R : Type u} [comm_ring R] {M N K : Module R} (m : M) (n : N) (k : K) :
((α_ M N K).inv) (m ⊗ₜ[R] (n ⊗ₜ[R] k)) = m ⊗ₜ[R] n ⊗ₜ[R] k