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
instance QuadraticModuleCat.instBraidedCategory {R : Type u} [CommRing R] [Invertible 2] :
CategoryTheory.BraidedCategory (QuadraticModuleCat R)
Equations
    source
    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
      source
      instance QuadraticModuleCat.instSymmetricCategory {R : Type u} [CommRing R] [Invertible 2] :
      CategoryTheory.SymmetricCategory (QuadraticModuleCat R)
      Equations