The symmetric monoidal structure on Module R.

noncomputable def ModuleCat.braiding {R : Type u} [CommRing R] (M : ModuleCat R) (N : ModuleCat R) : CategoryTheory.MonoidalCategory.tensorObj M N ≅ CategoryTheory.MonoidalCategory.tensorObj N M

(implementation) the braiding for R-modules

Equations

• ModuleCat.braiding M N = LinearEquiv.toModuleIso (TensorProduct.comm R ↑M ↑N)

@[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₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (ModuleCat.braiding Y₁ Y₂).hom = CategoryTheory.CategoryStruct.comp (ModuleCat.braiding X₁ X₂).hom (CategoryTheory.MonoidalCategory.tensorHom g f)

@[simp]

theorem ModuleCat.MonoidalCategory.braiding_naturality_left {R : Type u} [CommRing R] {X : ModuleCat R} {Y : ModuleCat R} (f : X ⟶ Y) (Z : ModuleCat R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (ModuleCat.braiding Y Z).hom = CategoryTheory.CategoryStruct.comp (ModuleCat.braiding X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Z f)

@[simp]

theorem ModuleCat.MonoidalCategory.braiding_naturality_right {R : Type u} [CommRing R] (X : ModuleCat R) {Y : ModuleCat R} {Z : ModuleCat R} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (ModuleCat.braiding X Z).hom = CategoryTheory.CategoryStruct.comp (ModuleCat.braiding X Y).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)

@[simp]

theorem ModuleCat.MonoidalCategory.hexagon_forward {R : Type u} [CommRing R] (X : ModuleCat R) (Y : ModuleCat R) (Z : ModuleCat R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.braiding X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (ModuleCat.braiding X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (ModuleCat.braiding X Z).hom))

@[simp]

theorem ModuleCat.MonoidalCategory.hexagon_reverse {R : Type u} [CommRing R] (X : ModuleCat R) (Y : ModuleCat R) (Z : ModuleCat R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (ModuleCat.braiding (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (ModuleCat.braiding Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.tensorHom (ModuleCat.braiding X Z).hom (CategoryTheory.CategoryStruct.id Y)))

noncomputable instance ModuleCat.MonoidalCategory.symmetricCategory {R : Type u} [CommRing R] : CategoryTheory.SymmetricCategory (ModuleCat R)

The symmetric monoidal structure on Module R.

Equations

• ModuleCat.MonoidalCategory.symmetricCategory = CategoryTheory.SymmetricCategory.mk

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