Documentation

Mathlib.Algebra.Category.AlgCat.Symmetric

The monoidal structure on AlgCat is symmetric. #

In this file we show:

source
🔸 coverage
@[implicit_reducible]
noncomputable instance AlgCat.instBraidedCategory {R : Type u} [CommRing R] :
CategoryTheory.BraidedCategory (AlgCat R)
source
🔸 coverage
@[implicit_reducible]
noncomputable instance AlgCat.instBraidedModuleCatForgetâ‚‚AlgHomCarrierLinearMapIdCarrier {R : Type u} [CommRing R] :
(CategoryTheory.forgetâ‚‚ (AlgCat R) (ModuleCat R)).Braided
source
🔸 coverage
@[implicit_reducible]
noncomputable instance AlgCat.instSymmetricCategory {R : Type u} [CommRing R] :
CategoryTheory.SymmetricCategory (AlgCat R)