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.

instance AlgebraCat.instBraidedModuleCatForget₂ {R : Type u} [CommRing R] : (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).Braided

Equations

• AlgebraCat.instBraidedModuleCatForget₂ = CategoryTheory.Functor.Braided.mk ⋯

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

Equations

• AlgebraCat.instSymmetricCategory = CategoryTheory.symmetricCategoryOfFaithful (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R))