(implementation) the braiding for R-modules
Equations
- M.braiding N = (tensor_product.comm R ↥M ↥N).to_Module_iso
@[protected, instance]
The symmetric monoidal structure on Module R
.
Equations
- Module.monoidal_category.symmetric_category = {to_braided_category := {braiding := Module.braiding _inst_1, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}, symmetry' := _}