Documentation

Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

The symmetric monoidal structure on Module R. #

source
🔸 coverage
def SemimoduleCat.braiding {R : Type u} [CommSemiring R] (M N : SemimoduleCat R) :
CategoryTheory.MonoidalCategoryStruct.tensorObj M N ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj N M

(implementation) the braiding for R-modules

Equations
    Instances For
      source
      📐 coverage
      @[simp]
      theorem SemimoduleCat.MonoidalCategory.braiding_naturality {R : Type u} [CommSemiring R] {X₁ X₂ Y₁ Y₂ : SemimoduleCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (Y₁.braiding Y₂).hom = CategoryTheory.CategoryStruct.comp (X₁.braiding X₂).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
      source
      📐 coverage
      @[simp]
      theorem SemimoduleCat.MonoidalCategory.braiding_naturality_left {R : Type u} [CommSemiring R] {X Y : SemimoduleCat R} (f : X ⟶ Y) (Z : SemimoduleCat R) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (Y.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
      source
      📐 coverage
      @[simp]
      theorem SemimoduleCat.MonoidalCategory.braiding_naturality_right {R : Type u} [CommSemiring R] (X : SemimoduleCat R) {Y Z : SemimoduleCat R} (f : Y ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (X.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
      source
      📐 coverage
      @[simp]
      theorem SemimoduleCat.MonoidalCategory.hexagon_forward {R : Type u} [CommSemiring R] (X Y Z : SemimoduleCat R) :
      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))
      source
      📐 coverage
      @[simp]
      theorem SemimoduleCat.MonoidalCategory.hexagon_reverse {R : Type u} [CommSemiring R] (X Y Z : SemimoduleCat R) :
      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))
      source
      🔸 coverage
      instance SemimoduleCat.MonoidalCategory.symmetricCategory {R : Type u} [CommSemiring R] :
      CategoryTheory.SymmetricCategory (SemimoduleCat R)

      The symmetric monoidal structure on Module R.

      Equations
        source
        📐 coverage
        @[simp]
        theorem SemimoduleCat.MonoidalCategory.braiding_hom_apply {R : Type u} [CommSemiring R] {M N : SemimoduleCat R} (m : ↑M) (n : ↑N) :
        (CategoryTheory.ConcreteCategory.hom (β_ M N).hom) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
        source
        📐 coverage
        @[simp]
        theorem SemimoduleCat.MonoidalCategory.braiding_inv_apply {R : Type u} [CommSemiring R] {M N : SemimoduleCat R} (m : ↑M) (n : ↑N) :
        (CategoryTheory.ConcreteCategory.hom (β_ M N).inv) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
        source
        📐 coverage
        theorem SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm {R : Type u} [CommSemiring R] {A B C D : SemimoduleCat R} :
        CategoryTheory.MonoidalCategory.tensorμ A B C D = ofHom ↑(TensorProduct.tensorTensorTensorComm R ↑A ↑B ↑C ↑D)
        source
        📐 coverage
        @[simp]
        theorem SemimoduleCat.MonoidalCategory.tensorμ_apply {R : Type u} [CommSemiring R] {A B C D : SemimoduleCat R} (x : ↑A) (y : ↑B) (z : ↑C) (w : ↑D) :
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.tensorμ A B C D)) (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) = x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w)
        source
        🔸 coverage
        instance ModuleCat.MonoidalCategory.instBraidedCategory {R : Type u} [CommRing R] :
        CategoryTheory.BraidedCategory (ModuleCat R)
        Equations
          source
          🔸 coverage
          instance ModuleCat.MonoidalCategory.instBraidedSemimoduleCatFunctorEquivalenceSemimoduleCat {R : Type u} [CommRing R] :
          equivalenceSemimoduleCat.functor.Braided
          Equations
            source
            🔸 coverage
            instance ModuleCat.MonoidalCategory.symmetricCategory {R : Type u} [CommRing R] :
            CategoryTheory.SymmetricCategory (ModuleCat R)
            Equations
              source
              📐 coverage
              @[simp]
              theorem ModuleCat.MonoidalCategory.braiding_hom_apply {R : Type u} [CommRing R] {M N : ModuleCat R} (m : ↑M) (n : ↑N) :
              (CategoryTheory.ConcreteCategory.hom (β_ M N).hom) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
              source
              📐 coverage
              @[simp]
              theorem ModuleCat.MonoidalCategory.braiding_inv_apply {R : Type u} [CommRing R] {M N : ModuleCat R} (m : ↑M) (n : ↑N) :
              (CategoryTheory.ConcreteCategory.hom (β_ M N).inv) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
              source
              📐 coverage
              theorem ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm {R : Type u} [CommRing R] {A B C D : ModuleCat R} :
              CategoryTheory.MonoidalCategory.tensorμ A B C D = ofHom ↑(TensorProduct.tensorTensorTensorComm R ↑A ↑B ↑C ↑D)
              source
              📐 coverage
              @[simp]
              theorem ModuleCat.MonoidalCategory.tensorμ_apply {R : Type u} [CommRing R] {A B C D : ModuleCat R} (x : ↑A) (y : ↑B) (z : ↑C) (w : ↑D) :
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.tensorμ A B C D)) (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) = x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w)