mathlib documentation

algebra.category.Module.monoidal.symmetric

The symmetric monoidal structure on Module R. #

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

(implementation) the braiding for R-modules

Equations
source
@[simp]
theorem Module.monoidal_category.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.monoidal_category.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.monoidal_category.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
@[protected, instance]
def Module.monoidal_category.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