Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory

Category-theoretic interpretations of CliffordAlgebra #

Main definitions #

@[simp]
theorem QuadraticModuleCat.cliffordAlgebra_obj_carrier {R : Type u} [CommRing R] (M : QuadraticModuleCat R) :
(QuadraticModuleCat.cliffordAlgebra.obj M) = CliffordAlgebra M.form
@[simp]
theorem QuadraticModuleCat.cliffordAlgebra_map {R : Type u} [CommRing R] {_M : QuadraticModuleCat R} {_N : QuadraticModuleCat R} (f : _M _N) :
QuadraticModuleCat.cliffordAlgebra.map f = CliffordAlgebra.map f.toIsometry

The "clifford algebra" functor, sending a quadratic R-module V to the clifford algebra on V.

This is CliffordAlgebra.map through the lens of category theory.

Equations
  • One or more equations did not get rendered due to their size.
Instances For