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/AlgebraCat/Symmetric.lean.

source
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.
source
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
Instances For
    source
    @[simp]
    theorem QuadraticModuleCat.toModuleCatBraidedFunctor_toMonoidalFunctor (R : Type u) [CommRing R] [Invertible 2] :
    (QuadraticModuleCat.toModuleCatBraidedFunctor R).toMonoidalFunctor = QuadraticModuleCat.toModuleCatMonoidalFunctor R
    source
    noncomputable instance QuadraticModuleCat.instFaithfulQuadraticModuleCatCategoryModuleCatToRingModuleCategoryToFunctorInstMonoidalCategoryMonoidalCategoryToLaxMonoidalFunctorToMonoidalFunctorInstBraidedCategoryQuadraticModuleCatCategoryInstMonoidalCategoryToBraidedCategorySymmetricCategoryToModuleCatBraidedFunctor {R : Type u} [CommRing R] [Invertible 2] :
    CategoryTheory.Faithful (QuadraticModuleCat.toModuleCatBraidedFunctor R).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
    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