The monoidal structure on QuadraticModuleCat is symmetric.

In this file we show:

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

Implementation notes

This file essentially mirrors Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean.

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

Equations

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

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

forget₂ (QuadraticModuleCat R) (ModuleCat R) is a braided functor.

Equations

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

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

Equations

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