Homotopy Type Theory Clifford algebra > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed


< Clifford algebra

Given a

commutative ring RR, a RR-pre-Clifford algebra is an RR-algebra AA with a canonical injection ι:RA\iota: R \to A and a quadratic form q:ARq:A \to R such that

a:Aaa=ι(q(a))\prod_{a:A} a \cdot a = \iota(q(a))

A RR-pre-Clifford algebra homomorphism between two RR-pre-Clifford algebras AA and BB is an RR-algebra homomorphism f:ABf:A \to B such that the quadratic form is preserved

a:Aq A(a)=q B(f(a))\prod_{a:A} q_A(a) = q_B(f(a))

The RR-Clifford algebra Cl(R,q)Cl(R, q) is the initial object in the category of RR-pre-Clifford algebras and RR-pre-Clifford algebra homomorphisms.

Suppose an nn-dimensional RR-Clifford algebra AA has a basis vector function e:U(n)Ae:U(n) \to A, where

U(n) i:i<nU(n) \coloneqq \sum_{i:\mathbb{N}} i \lt n

is the type of natural numbers less than nn, such that for all i:U(n)i:U(n), q(e i)=1q(e_i) = 1. Then qq is the standard diagonal form and AA is usually written as Cl n(R)Cl_n(R).

See also

Last revised on June 14, 2022 at 21:01:07. See the history of this page for a list of all contributions to it.