mathlib3 documentation

algebra.category.Module.monoidal.symmetric

The symmetric monoidal structure on Module R. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

(implementation) the braiding for R-modules

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