The monoidal structure on AlgCat is symmetric.

In this file we show:

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• AlgCat.instSymmetricCategory = CategoryTheory.SymmetricCategory.ofFaithful (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))