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