Documentation

Mathlib.Algebra.Category.AlgCat.Symmetric

The monoidal structure on AlgCat is symmetric. #

In this file we show:

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