mathlib documentation

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.

source
def Module.monoidal_category.tensor_obj {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :
Module R

(implementation) tensor product of R-modules

Equations
source
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') :
Module.monoidal_category.tensor_obj M M' ⟶ Module.monoidal_category.tensor_obj N N'

(implementation) tensor product of morphisms R-modules

Equations
source
theorem Module.monoidal_category.tensor_id {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :
Module.monoidal_category.tensor_hom (𝟙 M) (𝟙 N) = 𝟙 (Module.of R (↥M ⊗ ↥N))

source
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₂) :
Module.monoidal_category.tensor_hom (f₁ ≫ g₁) (f₂ ≫ g₂) = Module.monoidal_category.tensor_hom f₁ f₂ ≫ Module.monoidal_category.tensor_hom g₁ g₂

source
def Module.monoidal_category.associator {R : Type u} [comm_ring R] (M : Module R) (N : Module R) (K : Module R) :
Module.monoidal_category.tensor_obj (Module.monoidal_category.tensor_obj M N) K ≅ Module.monoidal_category.tensor_obj M (Module.monoidal_category.tensor_obj N K)

(implementation) the associator for R-modules

Equations
source
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₃) :
Module.monoidal_category.tensor_hom (Module.monoidal_category.tensor_hom f₁ f₂) f₃ ≫ (Module.monoidal_category.associator Y₁ Y₂ Y₃).hom = (Module.monoidal_category.associator X₁ X₂ X₃).hom ≫ Module.monoidal_category.tensor_hom f₁ (Module.monoidal_category.tensor_hom f₂ f₃)

source
theorem Module.monoidal_category.pentagon {R : Type u} [comm_ring R] (W : Module R) (X : Module R) (Y : Module R) (Z : Module R) :
Module.monoidal_category.tensor_hom (Module.monoidal_category.associator W X Y).hom (𝟙 Z) ≫ (Module.monoidal_category.associator W (Module.monoidal_category.tensor_obj X Y) Z).hom ≫ Module.monoidal_category.tensor_hom (𝟙 W) (Module.monoidal_category.associator X Y Z).hom = (Module.monoidal_category.associator (Module.monoidal_category.tensor_obj W X) Y Z).hom ≫ (Module.monoidal_category.associator W X (Module.monoidal_category.tensor_obj Y Z)).hom

source
def Module.monoidal_category.left_unitor {R : Type u} [comm_ring R] (M : Module R) :
Module.of R (R ⊗ ↥M) ≅ M

(implementation) the left unitor for R-modules

Equations
source
theorem Module.monoidal_category.left_unitor_naturality {R : Type u} [comm_ring R] {M N : Module R} (f : M ⟶ N) :
Module.monoidal_category.tensor_hom (𝟙 (Module.of R R)) f ≫ (Module.monoidal_category.left_unitor N).hom = (Module.monoidal_category.left_unitor M).hom ≫ f

source
def Module.monoidal_category.right_unitor {R : Type u} [comm_ring R] (M : Module R) :
Module.of R (↥M ⊗ R) ≅ M

(implementation) the right unitor for R-modules

Equations
source
theorem Module.monoidal_category.right_unitor_naturality {R : Type u} [comm_ring R] {M N : Module R} (f : M ⟶ N) :
Module.monoidal_category.tensor_hom f (𝟙 (Module.of R R)) ≫ (Module.monoidal_category.right_unitor N).hom = (Module.monoidal_category.right_unitor M).hom ≫ f

source
theorem Module.monoidal_category.triangle {R : Type u} [comm_ring R] (M N : Module R) :
(Module.monoidal_category.associator M (Module.of R R) N).hom ≫ Module.monoidal_category.tensor_hom (𝟙 M) (Module.monoidal_category.left_unitor N).hom = Module.monoidal_category.tensor_hom (Module.monoidal_category.right_unitor M).hom (𝟙 N)

source
@[instance]
def Module.Module.monoidal_category {R : Type u} [comm_ring R] :
category_theory.monoidal_category (Module R)

Equations
source
@[instance]
def Module.comm_ring {R : Type u} [comm_ring R] :
comm_ring ↥(𝟙_ (Module R))

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

Equations
source
@[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

source
@[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

source
@[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

source
@[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

source
def Module.braiding {R : Type u} [comm_ring R] (M : Module R) (N : Module R) :
Module.monoidal_category.tensor_obj M N ≅ Module.monoidal_category.tensor_obj N M

(implementation) the braiding for R-modules

Equations
source
@[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)

source
@[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)

source
@[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)

source
@[instance]
def Module.Module.symmetric_category {R : Type u} [comm_ring R] :
category_theory.symmetric_category (Module R)

The symmetric monoidal structure on Module R.

Equations
source
@[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

source
@[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