The Blueprint For Formalizing Geometric Algebra in Lean: Definition

2.1 Definition

Let $M$ be a module over a commutative ring $R$, equipped with a quadratic form $Q: M \to R$.

Definition 2.1.1 Clifford algebra

✓

Let $\iota : M \to _{l[R]} T(M)$ be the canonical $R$-linear map for the tensor algebra $T(M)$.

Let $\mathit{1}: R \to _{+*}T(M)$ be the canonical map from $R$ to $T(M)$, as a ring homomorphism.

A Clifford algebra over $Q$, denoted $\mathop{\mathcal{C}\ell }(Q)$, is the ring quotient of the tensor algebra $T(M)$ by the equivalence relation satisfying $\iota (m)^2 \sim \mathit{1}(Q(m))$ for all $m \in M$.

The natural quotient map is denoted $\pi : T(M) \to \mathop{\mathcal{C}\ell }(Q)$ in some literatures, or $\pi _\Phi $/$\pi _Q$ to emphasize the bilinear form $\Phi $ or the quadratic form $Q$, respectively.

Remark 2.1.2

In literatures, $M$ is often written $V$, and the quotient is taken by the two-sided ideal $I_Q$ generated from the set $\{ v \otimes v - Q(v) \: \vert \: v \in V \} $.

As of writing, Mathlib does not have direct support for two-sided ideals, but it does support the equivalent operation of taking the ring quotient by a suitable closure of a relation like $v \otimes v \sim Q(v)$.

Hence the definition above.

Remark 2.1.3

This definition and what follows in Mathlib is initially presented in [ Wieser and Song(2022) ] , some further developments are based on [ Grinberg(2016) ] , and in turn based on [ Bourbaki(2007) ] which is in French and never translated to English.

The most informative English reference on [ Bourbaki(2007) ] is
[ Jadczyk(2019) ] , which has an updated exposition in [ Jadczyk(2023) ] .

Example 2.1.4 Clifford algebra over a vector space

Let $V$ be a vector space $\mathbb R^n$ over $\mathbb R$, equipped with a quadratic form $Q$.

Since $\mathbb R$ is a commutative ring and $V$ is a module, definition 2.1.1 of Clifford algebra applies.

Definition 2.1.5 Clifford map

✓

We denote the canonical $R$-linear map to the Clifford algebra $\mathop{\mathcal{C}\ell }(M)$ by $\iota : M \to _{l[R]} \mathop{\mathcal{C}\ell }(M)$.

It’s denoted $i_\Phi $ or just $i$ in some literatures.

Definition 2.1.6 Clifford lift

✓

Given a linear map $f : M \to _{l[R]} A$ into an $R$-algebra $A$, satisfying $f(m)^2 = Q(m)$ for all $m \in M$, called is Clifford, the canonical lift of $f$ is defined to be a algebra homomorphism from $\mathop{\mathcal{C}\ell }(Q)$ to $A$, denoted $\operatorname {lift} f : \mathop{\mathcal{C}\ell }(Q) \to _{a}A$.

Theorem 2.1.7 Universal property

✓

Given $f : M \to _{l[R]} A$, which is Clifford, $F = \operatorname {lift} f$ (denoted $\bar{f}$ in some literatures), we have:

1) $F \circ \iota = f$, i.e. the following diagram commutes:

$\begin{tikzcd} [column sep=huge, row sep=huge] \Cl(Q) \arrow[r, "F = \operatorname{lift} f"] & A \\ V \arrow[ru, "f"'] \arrow[u, "\iota"] \end{tikzcd}$

2) $\operatorname {lift}$ is unique, i.e. given $G : \mathop{\mathcal{C}\ell }(Q) \to _{a}A$, we have:

$ G \circ \iota = f \iff G = \operatorname {lift} f$

Remark 2.1.8

The universal property of the Clifford algebras is now proven, and should be used instead of the definition that is subject to change.

Definition 2.1.9 Exterior algebra

✓

An Exterior algebra over $M$ is the Clifford algebra $\mathop{\mathcal{C}\ell }(Q)$ where $Q(m) = 0$ for all $m \in M$.