Documentation

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric

The monoidal structure on QuadraticModuleCat is symmetric. #

In this file we show:

Implementation notes #

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

source
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.
source
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
  • One or more equations did not get rendered due to their size.
source
noncomputable instance QuadraticModuleCat.instSymmetricCategory {R : Type u} [CommRing R] [Invertible 2] :
CategoryTheory.SymmetricCategory (QuadraticModuleCat R)
Equations