Documentation

Mathlib.Algebra.Category.AlgCat.Symmetric

The monoidal structure on AlgCat is symmetric. #

In this file we show:

source
instance AlgCat.instBraidedCategory {R : Type u} [CommRing R] :
CategoryTheory.BraidedCategory (AlgCat R)
Equations
    source
    instance AlgCat.instBraidedModuleCatForget₂ {R : Type u} [CommRing R] :
    (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).Braided
    Equations
      source
      instance AlgCat.instSymmetricCategory {R : Type u} [CommRing R] :
      CategoryTheory.SymmetricCategory (AlgCat R)
      Equations