# The symmetric monoidal structure on Module R. #

noncomputable def ModuleCat.braiding {R : Type u} [] (M : ) (N : ) :

(implementation) the braiding for R-modules

Equations
Instances For
@[simp]
theorem ModuleCat.MonoidalCategory.braiding_naturality {R : Type u} [] {X₁ : } {X₂ : } {Y₁ : } {Y₂ : } (f : X₁ Y₁) (g : X₂ Y₂) :
CategoryTheory.CategoryStruct.comp (Y₁.braiding Y₂).hom = CategoryTheory.CategoryStruct.comp (X₁.braiding X₂).hom
@[simp]
theorem ModuleCat.MonoidalCategory.braiding_naturality_left {R : Type u} [] {X : } {Y : } (f : X Y) (Z : ) :
@[simp]
theorem ModuleCat.MonoidalCategory.braiding_naturality_right {R : Type u} [] (X : ) {Y : } {Z : } (f : Y Z) :
noncomputable instance ModuleCat.MonoidalCategory.symmetricCategory {R : Type u} [] :

The symmetric monoidal structure on Module R.

Equations
• ModuleCat.MonoidalCategory.symmetricCategory =
@[simp]
theorem ModuleCat.MonoidalCategory.braiding_hom_apply {R : Type u} [] {M : } {N : } (m : M) (n : N) :
(β_ M N).hom (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
@[simp]
theorem ModuleCat.MonoidalCategory.braiding_inv_apply {R : Type u} [] {M : } {N : } (m : M) (n : N) :
(β_ M N).inv (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
theorem ModuleCat.MonoidalCategory.tensor_μ_eq_tensorTensorTensorComm {R : Type u} [] {A : } {B : } {C : } {D : } :
CategoryTheory.tensor_μ () (A, B) (C, D) = (TensorProduct.tensorTensorTensorComm R A B C D)
@[simp]
theorem ModuleCat.MonoidalCategory.tensor_μ_apply {R : Type u} [] {A : } {B : } {C : } {D : } (x : A) (y : B) (z : C) (w : D) :
(CategoryTheory.tensor_μ () (A, B) (C, D)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z ⊗ₜ[R] w) = (x ⊗ₜ[R] z) ⊗ₜ[R] y ⊗ₜ[R] w