Category-theoretic interpretations of CliffordAlgebra #

Main definitions #

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

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

This is through the lens of category theory.

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