Category-theoretic interpretations of CliffordAlgebra

Main definitions

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

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.

@[simp]

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

@[simp]

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