Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

The symmetric monoidal structure on Module R. #

(implementation) the braiding for R-modules

Equations
Instances For
    @[simp]
    theorem ModuleCat.MonoidalCategory.braiding_naturality {R : Type u} [CommRing R] {X₁ : ModuleCat R} {X₂ : ModuleCat R} {Y₁ : ModuleCat R} {Y₂ : ModuleCat R} (f : X₁ Y₁) (g : X₂ Y₂) :

    The symmetric monoidal structure on Module R.

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