Documentation

Mathlib.Algebra.Category.AlgebraCat.Symmetric

The monoidal structure on AlgebraCat is symmetric. #

In this file we show:

source
instance AlgebraCat.instBraidedCategoryAlgebraCatInstCategoryAlgebraCatInstMonoidalCategory {R : Type u} [CommRing R] :
CategoryTheory.BraidedCategory (AlgebraCat R)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraCat.toModuleCatBraidedFunctor_toMonoidalFunctor (R : Type u) [CommRing R] :
(AlgebraCat.toModuleCatBraidedFunctor R).toMonoidalFunctor = AlgebraCat.toModuleCatMonoidalFunctor R
source
def AlgebraCat.toModuleCatBraidedFunctor (R : Type u) [CommRing R] :
CategoryTheory.BraidedFunctor (AlgebraCat R) (ModuleCat R)

forgetâ‚‚ (AlgebraCat R) (ModuleCat R) as a braided functor.

Equations
Instances For
    source
    instance AlgebraCat.instFaithfulAlgebraCatInstCategoryAlgebraCatModuleCatToRingModuleCategoryToFunctorInstMonoidalCategoryMonoidalCategoryToLaxMonoidalFunctorToMonoidalFunctorInstBraidedCategoryAlgebraCatInstCategoryAlgebraCatInstMonoidalCategoryToBraidedCategorySymmetricCategoryToModuleCatBraidedFunctor {R : Type u} [CommRing R] :
    CategoryTheory.Faithful (AlgebraCat.toModuleCatBraidedFunctor R).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance AlgebraCat.instSymmetricCategory {R : Type u} [CommRing R] :
    CategoryTheory.SymmetricCategory (AlgebraCat R)
    Equations