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.instBraidedCategoryQuadraticModuleCatCategoryInstMonoidalCategory {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 def QuadraticModuleCat.toModuleCatBraidedFunctor (R : Type u) [CommRing R] [Invertible 2] : CategoryTheory.BraidedFunctor (QuadraticModuleCat R) (ModuleCat R)

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

Equations

• QuadraticModuleCat.toModuleCatBraidedFunctor R = { toMonoidalFunctor := QuadraticModuleCat.toModuleCatMonoidalFunctor R, braided := ⋯ }

@[simp]

theorem QuadraticModuleCat.toModuleCatBraidedFunctor_toMonoidalFunctor (R : Type u) [CommRing R] [Invertible 2] : (QuadraticModuleCat.toModuleCatBraidedFunctor R).toMonoidalFunctor = QuadraticModuleCat.toModuleCatMonoidalFunctor R

noncomputable instance QuadraticModuleCat.instFaithfulQuadraticModuleCatCategoryModuleCatToRingModuleCategoryToFunctorInstMonoidalCategoryMonoidalCategoryToLaxMonoidalFunctorToMonoidalFunctorInstBraidedCategoryQuadraticModuleCatCategoryInstMonoidalCategoryToBraidedCategorySymmetricCategoryToModuleCatBraidedFunctor {R : Type u} [CommRing R] [Invertible 2] : CategoryTheory.Functor.Faithful (QuadraticModuleCat.toModuleCatBraidedFunctor R).toFunctor

Equations

• ⋯ = ⋯

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

Equations

• QuadraticModuleCat.instSymmetricCategory = CategoryTheory.symmetricCategoryOfFaithful (QuadraticModuleCat.toModuleCatBraidedFunctor R)