The monoidal structure on AlgebraCat is symmetric.

In this file we show:

• AlgebraCat.instSymmetricCategory : SymmetricCategory (AlgebraCat.{u} R)

instance AlgebraCat.instBraidedCategory {R : Type u} [CommRing R] : CategoryTheory.BraidedCategory (AlgebraCat R)

Equations

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

@[simp]

theorem AlgebraCat.toModuleCatBraidedFunctor_toMonoidalFunctor (R : Type u) [CommRing R] : (AlgebraCat.toModuleCatBraidedFunctor R).toMonoidalFunctor = AlgebraCat.toModuleCatMonoidalFunctor R

def AlgebraCat.toModuleCatBraidedFunctor (R : Type u) [CommRing R] : CategoryTheory.BraidedFunctor (AlgebraCat R) (ModuleCat R)

forget₂ (AlgebraCat R) (ModuleCat R) as a braided functor.

Equations

• AlgebraCat.toModuleCatBraidedFunctor R = { toMonoidalFunctor := AlgebraCat.toModuleCatMonoidalFunctor R, braided := ⋯ }

instance AlgebraCat.instFaithfulModuleCatToModuleCatBraidedFunctor {R : Type u} [CommRing R] : (AlgebraCat.toModuleCatBraidedFunctor R).Faithful

Equations

• ⋯ = ⋯

instance AlgebraCat.instSymmetricCategory {R : Type u} [CommRing R] : CategoryTheory.SymmetricCategory (AlgebraCat R)

Equations

• AlgebraCat.instSymmetricCategory = CategoryTheory.symmetricCategoryOfFaithful (AlgebraCat.toModuleCatBraidedFunctor R)