Category-theoretic interpretations of clifford_algebra

Main definitions

• QuadraticModuleCat.cliffordAlgebra: the functor from quadratic modules to algebras

@[simp]

theorem QuadraticModuleCat.cliffordAlgebra_map {R : Type u} [CommRing R] {_M : QuadraticModuleCat R} {_N : QuadraticModuleCat R} (f : _M ⟶ _N) : QuadraticModuleCat.cliffordAlgebra.toPrefunctor.map f = CliffordAlgebra.map f.toIsometry

@[simp]

theorem QuadraticModuleCat.cliffordAlgebra_obj_carrier {R : Type u} [CommRing R] (M : QuadraticModuleCat R) : ↑(QuadraticModuleCat.cliffordAlgebra.toPrefunctor.obj M) = CliffordAlgebra M.form

def QuadraticModuleCat.cliffordAlgebra {R : Type u} [CommRing R] : CategoryTheory.Functor (QuadraticModuleCat R) (AlgebraCat R)

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.