The symmetric monoidal structure on Module R.

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

(implementation) the braiding for R-modules

Equations

• Eq (M.braiding N) (TensorProduct.comm R M.carrier N.carrier).toModuleIso

theorem ModuleCat.MonoidalCategory.braiding_naturality {R : Type u} [CommRing R] {X₁ X₂ Y₁ Y₂ : ModuleCat R} (f : Quiver.Hom X₁ Y₁) (g : Quiver.Hom X₂ Y₂) : Eq (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (Y₁.braiding Y₂).hom) (CategoryTheory.CategoryStruct.comp (X₁.braiding X₂).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom g f))

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

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

theorem ModuleCat.MonoidalCategory.hexagon_forward {R : Type u} [CommRing R] (X Y Z : ModuleCat R) : Eq (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (X.braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.braiding Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (X.braiding Z).hom)))

theorem ModuleCat.MonoidalCategory.hexagon_reverse {R : Type u} [CommRing R] (X Y Z : ModuleCat R) : Eq (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).braiding Z).hom (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (Y.braiding Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (X.braiding Z).hom Y)))

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

The symmetric monoidal structure on Module R.

Equations

• One or more equations did not get rendered due to their size.

theorem ModuleCat.MonoidalCategory.braiding_hom_apply {R : Type u} [CommRing R] {M N : ModuleCat R} (m : M.carrier) (n : N.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.BraidedCategory.braiding M N).hom) (TensorProduct.tmul R m n)) (TensorProduct.tmul R n m)

theorem ModuleCat.MonoidalCategory.braiding_inv_apply {R : Type u} [CommRing R] {M N : ModuleCat R} (m : M.carrier) (n : N.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.BraidedCategory.braiding M N).inv) (TensorProduct.tmul R n m)) (TensorProduct.tmul R m n)

theorem ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm {R : Type u} [CommRing R] {A B C D : ModuleCat R} : Eq (CategoryTheory.MonoidalCategory.tensorμ A B C D) (ofHom (TensorProduct.tensorTensorTensorComm R A.carrier B.carrier C.carrier D.carrier).toLinearMap)

theorem ModuleCat.MonoidalCategory.tensorμ_apply {R : Type u} [CommRing R] {A B C D : ModuleCat R} (x : A.carrier) (y : B.carrier) (z : C.carrier) (w : D.carrier) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.tensorμ A B C D)) (TensorProduct.tmul R (TensorProduct.tmul R x y) (TensorProduct.tmul R z w))) (TensorProduct.tmul R (TensorProduct.tmul R x z) (TensorProduct.tmul R y w))