mathlibdocumentation

algebra.category.Module.monoidal

The symmetric 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 and then the symmetric_category instance.

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

Equations
def Module.monoidal_category.tensor_hom {R : Type u} [comm_ring R] {M N : Module R} {M' N' : Module R} (f : M N) (g : M' N') :

(implementation) tensor product of morphisms R-modules

Equations
theorem Module.monoidal_category.tensor_id {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :
= 𝟙 (M N))
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₂) :
(f₂ g₂) =
def Module.monoidal_category.associator {R : Type u} [comm_ring R] (M : Module R) (N : Module R) (K : Module R) :

(implementation) the associator for R-modules

Equations

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₃) :
theorem Module.monoidal_category.pentagon {R : Type u} [comm_ring R] (W : Module R) (X : Module R) (Y : Module R) (Z : Module R) :
def Module.monoidal_category.left_unitor {R : Type u} [comm_ring R] (M : Module R) :
(R M) M

(implementation) the left unitor for R-modules

Equations
theorem Module.monoidal_category.left_unitor_naturality {R : Type u} [comm_ring R] {M N : Module R} (f : M N) :
def Module.monoidal_category.right_unitor {R : Type u} [comm_ring R] (M : Module R) :
(M R) M

(implementation) the right unitor for R-modules

Equations
theorem Module.monoidal_category.right_unitor_naturality {R : Type u} [comm_ring R] {M N : Module R} (f : M N) :
theorem Module.monoidal_category.triangle {R : Type u} [comm_ring R] (M N : Module R) :
@[protected, instance]

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

Equations
@[simp]
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
@[simp]
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
@[simp]
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
@[simp]
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
@[simp]
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
@[simp]
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)
@[simp]
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
def Module.braiding {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :

(implementation) the braiding for R-modules

Equations
@[simp]
theorem Module.braiding_naturality {R : Type u} [comm_ring R] {X₁ X₂ Y₁ Y₂ : Module R} (f : X₁ Y₁) (g : X₂ Y₂) :
(f g) (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom (g f)
@[simp]
theorem Module.hexagon_forward {R : Type u} [comm_ring R] (X Y Z : Module R) :
(α_ X Y Z).hom (X.braiding (Y Z)).hom (α_ Y Z X).hom = ((X.braiding Y).hom 𝟙 Z) (α_ Y X Z).hom (𝟙 Y (X.braiding Z).hom)
@[simp]
theorem Module.hexagon_reverse {R : Type u} [comm_ring R] (X Y Z : Module R) :
(α_ X Y Z).inv ((X Y).braiding Z).hom (α_ Z X Y).inv = (𝟙 X (Y.braiding Z).hom) (α_ X Z Y).inv ((X.braiding Z).hom 𝟙 Y)
@[protected, instance]
def Module.symmetric_category {R : Type u} [comm_ring R] :

The symmetric monoidal structure on Module R.

Equations
@[simp]
theorem Module.monoidal_category.braiding_hom_apply {R : Type u} [comm_ring R] {M N : Module R} (m : M) (n : N) :
((β_ M N).hom) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
@[simp]
theorem Module.monoidal_category.braiding_inv_apply {R : Type u} [comm_ring R] {M N : Module R} (m : M) (n : N) :
((β_ M N).inv) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n