Dude, where's my basis?

The universal property of the Clifford algebra

Eric Wieser
Cambridge University Engineering Department

slides: eric-wieser.github.io/brno-2021 2021-11-30

A recap on bases

A basis over a vector space $V$ is a family of vectors ${e_1, \ldots, e_n}$, such that for any vector $\vec{v} : V$, there is a unique choice of scalars $\sca{a_i}$ satisfying $\vec{v} = \sum_{i=1}^n \sca{a_i}\vec{e_i}$ (e.g., $\vec{v} = \sca{x}\vec{i} + \sca{y}\vec{j} + \sca{z}\vec{k}$).

Uniqueness can also be stated as $\vec{e_i}$ being linearly independent.

There exists a basis for any vector space (even infinite-dimensional!).

Usually many possible choices of basis!

Bases for a geometric algebra

If $V$ has a basis $\vec{e_i}$, then $\mathcal{G}(V)$ usually has both of the following bases:

  • $e_s = \prod_{i \in s} e_i$
  • $e_s = \bigwedge_{i \in s} e_i$, often written $e_{123} = e_{\{1,2,3\}} = e_1\wedge e_2\wedge e_3$

Using the second case, any multivector $x$ in $\mathcal{G}(V)$ where $V$ has basis $\{\vec{e_1}, \vec{e_2}, \vec{e_3}\}$ can be written:

\begin{alignat}{2} x &= \sca{x_\emptyset} &&+ \sca{x_1}e_1 + \sca{x_2}e_2 + \sca{x_2}e_2 \\ &+ \sca{x_{12}}e_{12} + \sca{x_{23}}e_{23} + \sca{x_{13}}e_{13} &&+ \sca{x_{123}}e_{123} \end{alignat}

(A note on colors in this talk: $\sca{a_i}$ for scalars, $\vec{e_i}$ for vectors, $e_i$ for multivectors)

A recap on basesBasis-dependence of algorithms

Algorithms fall into one of three categories:


The choice of basis affects the result

  • Taxicab distance / $L^\infty$-norm
  • Cross product (consider handedness)
  • Pseudoscalar $I$ in GA (handedness and magnitude)


The computation needs a basis, but the outcome isn't affected by the choice.

  • Trace and determinant of a linear operator
  • Vee product $a \vee b$ (signs cancel)


The entire computation can be done without reference to a basis

  • Addition / subtraction (axiomatically)
  • Application of the universal property (this talk!)

Why do we care?

In the language of GA: these aren't covariant, meaning they don't behave the same way on transformed objects.

Proving these algorithms are covariant can be tricky.

These are covariant by construction!

In more exotic constructions, sometimes there is no basis at all!

A recap on Geometric Algebra

What do we mean by the $\mathbb{R}^{p,q,r}$ in $\mathcal{G}(\mathbb{R}^{p,q,r})$?

A space spanned by the orthogonal basis $\{\vec{e^{+}_1}, \cdots, \vec{e^{+}_p}, \vec{e^{-}_1}, \cdots, \vec{e^{-}_q}, \vec{e^{0}_1}, \cdots, \vec{e^{0}_r}\}$; orthogonal $\implies \vec{e_i} \cdot \vec{e_j} = \sca{0}$ for $i \ne j$, and basis $\implies \vec{v} = \sum_{i=1}^p \sca{a^{+}_i}\vec{e^{+}_i} + \sum_{i=1}^q \sca{a^{-}_i}\vec{e^{-}_i} + \sum_{i=1}^r \sca{a^{0}_i}\vec{e^{0}_i}$ for all vectors $\vec{v}$.

Additionally, the ${}^{p,q,r}$ tells us $\vec{e^{+}_i} \cdot \vec{e^{+}_i} = \sca{1}$, $\vec{e^{-}_i} \cdot \vec{e^{-}_i} = \sca{-1}$, $\vec{e^{0}_i} \cdot \vec{e^{0}_i} = \sca{0}$,

What's a quadratic form?

The $(\vec{v} \cdots \vec{v})^2$ above describes a quadratic form with $\Qof{e^{+}_i} = \sca{1}, \Qof{e^{-}_i} = \sca{-1}, \Qof{e^{0}_i} = \sca{0}$ instead. For the above basis:

$$\Qof{v} = \sum_{i=1}^p \sca{{(a^{+}_i)}^2} - \sum_{i=1}^q \sca{{(a^{-}_i)}^2}$$

More generally, a quadratic form is a function $Q : V \to R$ such that when we define $\Bof{x}{y}$ as $\sca{\Qof{x + y} - \Qof{x} - \Qof{y}}$:

\begin{align} \Qof{\sca{a}x} &= \sca{a^2}\Qof{x}, & \Bof{x_1 + x_2}{y} &= \sca{\Bof{x_1}{y} + \Bof{x_2}{y}}, & \Bof{\sca{a}x}{y} &= \sca{a}\Bof{x}{y} \\ && \Bof{x}{y_1 + y_2} &= \sca{\Bof{x}{y_1} + \Bof{x}{y_2}}, & \Bof{x}{\sca{a}y} &= \sca{a}\Bof{x}{y} \end{align}

Intuition: $Q(x)$ is the squared magnitude of $x$, from which we can obtain $\Bof{x}{y} = \sca{2(}\vec{x} \cdot \vec{y}\sca{)}$.

Instead of talking about $\mathcal{G}(\mathbb{R}^{p,q,r})$ which names a basis, let's talk more generally about $\mathcal{G}(V, Q)$ which doesn't name a basis; the geometric algebra over a vector space $V$ with quadratic form $Q$.

A recap on Geometric AlgebraDefining the product

The orthogonal basis approach
  • Start with an orthogonal basis over $V$, $e_i$, and allow these to be freely multiplied.
  • Orthogonal vectors anticommute, so $e_ie_j = -e_je_i$ when $i \ne j$.
  • Vectors with the same index produce a scalar, $e_i^2 = \Qof{e_i}1$.

The above relations let us reduce any product of basis vectors, eg $e_1e_2e_1 = e_1(-e_1e_2) = -\Qof{e_1}e_2$

More formally: the quotient approach

Start with the tensor algebra $T(V) = \bigoplus_{n=0}^\infty V^{\otimes n} = R \oplus V \oplus (V \otimes V) + \cdots$ that lets us multiply vectors freely provided that $(\sca{a}x) \times y = \sca{a}(x \times y) = x \times (\sca{a}y)$.

Define $\mathcal{I}$ as the set of elements of $T(V)$ of the form $v^2 - \Qv1$, where $\vec{v} : V$ is any vector (not necessarily a basis vector), and $v$ is that same vector as an element of $T(V)$. Extend $\mathcal{I}$ to be a two-sided ideal; that is add elements to satisfy:

\begin{align} 0 &\in \mathcal{I}, & \forall x \forall y, x \in \mathcal{I}, y \in \mathcal{I} \implies x + y &\in \mathcal{I}, & \forall x \forall y, x \in \mathcal{I} \implies xy \in \mathcal{I}, yx \in \mathcal{I}. \end{align}

Define $\mathcal{G}(Q, V)$ as the quotient of $T(V)$ by $\mathcal{I}$; that is, consider two elements $x, y : T(V)$ as equal if $x - y \in \mathcal{I}$. We can recover the same rules as above; in the $i \ne j$ case,

\begin{align} e_ie_j - (-e_je_i) &= e_ie_j + e_je_i = (e_i + e_j)^2 - e_i^2 - e_j^2 \\ &= \underbrace{\left((e_i + e_j)^2 - \Qof{e_i+e_j}1\right)}_{\in \mathcal{I}}- \underbrace{\left(e_i^2 - \Qof{e_i}1\right)}_{\in \mathcal{I}} - \underbrace{\left(e_j^2 - \Qof{e_j}1\right)}_{\in \mathcal{I}} + \underbrace{\sca{\left(\Qof{e_i+e_j} - \Qof{e_i} - \Qof{e_j}\right)}}_{{}=\Bof{e_i}{e_j}=\sca{0}}1 \end{align}
\begin{align} \implies e_ie_j - (-e_je_i) &\in \mathcal{I} \end{align}

Abstract algebra

Abstract algebraStructures


We say $R$ is a ring if it has $0$,$+$,$-$,$1$,$\times$, and they satisfy some basic rules of arithmetic:

\begin{align} x + 0 &= x, & 0 + x &= x, & x + (y + z) &= (x + y) + z, & x + y &= y + x, & -x + x &= 0 \\ x \times 1 &= x, & 1 \times x &= x, & x \times (y \times z) &= (x \times y) \times z & {\color{gray} (x \times y} &{\color{gray} {}= y \times x)}{\color{red} ?^1} \\ x \times 0 &= 0, & 0 \times x &= 0, & x \times (y + z) &= x\times y + x \times z, & {\color{gray} (x \times y} &{\color{gray} {}= x \times z \implies y = z)}{\color{red} ?^2}\\ && && (x + y) \times z &= x\times z + y\times z \end{align}

Multiplication is not necessarily commutative1 or cancellative2! If we add an inverse (${}^{-1}$), this is a division ring or field when also commutative.


  • $\mathbb{Z}$ (commutative ring)
  • $\mathbb{Q}$ (field)
  • $\mathbb{R}$ (field)
  • $\mathbb{H}$ (division ring)

We say $M$ is an $R$-module if it has $0$, $+$, and scalar multiplication by elements of a ring $R$ satisfying:

\begin{align} x + 0 &= x, & 0 + x &= x, & x + (y + z) &= (x + y) + z, & x + y &= y + x \\ \sca{0}x &= 0, & \sca{a}0 &= 0, & \sca{(a + b)}x &= \sca{a}x + \sca{b}x, & \sca{a}(x + y) &= \sca{a}x + \sca{a}y \\ \sca{1}x &= x, & & & \sca{(a \times b)}x &= \sca{a}(\sca{b}x) \end{align}

When $R$ is not only a ring but a field, we call this a vector space. Every vector space has a basis, but not every module does!


  • $\mathbb{Z}^3$ is a $\mathbb{Z}$-module
  • $\mathbb{R}^3$ is an $\mathbb{R}$-vector space
  • $\mathbb{C}$ is an $\mathbb{R}$-vector space

We say that $A$ is an $R$-algebra if it is both a ring and an $R$-module, and additionally satisfies:

\begin{align} \sca{a}(x \times y) = (\sca{a}x) \times y = x \times (\sca{a}y) \end{align}
that is, the scalar multiplication commutes and associates with regular multiplication.


  • $\mathbb{Q}$ is a $\mathbb{Z}$-algebra
  • $\mathbb{C}$ is an $\mathbb{R}$-algebra
  • $\mathcal{G}(\mathbb{R}^n)$ is an $\mathbb{R}$-algebra

Abstract algebraMorphisms

$R$-linear map

We say $f : M \to N$ is an $R$-linear map if $M$ and $N$ are $R$-modules, and the map satisfies: \begin{align} f(0) &= 0, & f(x + y) &= f(x) + f(y), & f(\sca{a}x) = \sca{a}f(x) \end{align}

We'll write this as $f : M \lin{R} N$.


  • Rotating a point in $\mathbb{R}^2$ by a fixed angle around the origin.
  • $f = x \mapsto -x$, negation
  • $f = x \mapsto {\tilde x}$, grade reversal
$R$-algebra morphism

We say $f : A \to B$ is an $R$-algebra morphism if $A$ and $B$ are $R$-algebras, and $f$ is a linear map that additionally satisfies: \begin{align} f(1) &= 1, & f(x \times y) &= f(x) \times f(y) \end{align}

We'll write this as $f : A \alg{R} B$.


  • $f = x \mapsto x$, the identity,
  • $f = x \mapsto R^{-1}xR$, the sandwich product of a fixed rotor on a multivector.
  • $f = x \mapsto {\hat x}$, grade involution.

The universal property

For any choice of an $R$-algebra $A$, there is one-to-one correspondence we'll call $\operatorname{lift}$ between

$f : V \lin{R} A$ where $f(\vec{v})^2 = \sca{Q(}v\sca{)}1$
$F : \mathcal{G}(V, Q) \alg{R} A$

$F = \operatorname{lift}[f]$ and $f = \operatorname{lift}^{-1}[F]$

When $F_2 : A \alg{R} A_2$, $\operatorname{lift}[F_2 \circ f] = F_2 \circ F$ and $\operatorname{lift}^{-1}[F_2 \circ F] = F_2 \circ f$.

Substituting: $\operatorname{lift}[F_2 \circ f] = F_2 \circ \operatorname{lift}[f]$ and $\operatorname{lift}^{-1}[F_2 \circ F] = F_2 \circ \operatorname{lift}^{-1}[F]$.

The universal propertyRecovering the generator $\iota(\vec{v})$

Choose $A = \mathcal{G}(V, Q)$, $F = (x \mapsto x)$ to obtain:

Read off $F_2 \circ \iota = \operatorname{lift}^{-1}[F_2]$ for any $F_2$

Choose $F_2 = \operatorname{lift}[f_2]$ for some $f_2$ to get: \begin{align} \operatorname{lift}[f_2] \circ \iota &= \operatorname{lift}^{-1}[\operatorname{lift}[f_2]] \\ &= f_2 \\ \implies \operatorname{lift}[f_2](\iota(\vec{v})) &= f_2(\vec{v}) \\ \end{align}

$\iota = \operatorname{lift}^{-1}[x \mapsto x]$ is the output of $\operatorname{lift}^{-1}$,
so satisies $\iota(\vec{v})^2 = \Qof{v}1$.

Key results and intuition

$\operatorname{lift}[f_2](\iota(\vec{v})) = f_2(\vec{v})$ $\operatorname{lift}[f]$ is like the outermorphism of $f$, but with the geometric product instead of the wedge product. As an example:

\begin{align} \operatorname{lift}[f](\iota(\vec{u})\times\iota(\vec{v}) + \iota(\vec{w}) + \sca{c}1) &= f(\vec{u}) \times f(\vec{v}) + f(\vec{w}) + \sca{c}1. \end{align}

$\iota(\vec{v})^2 = \Qof{v}1$ $\iota : V \lin{R} \mathcal{G}(V, Q)$ is the natural embedding of the vectors into the geometric algebra.

The universal propertyExtensionality

Consider two algebra morphisms $F_1, F_2 : \mathcal{G}(V, Q) \alg{R} A$. We wish to show that $F_1 = F_2$.

Function extensionality is the statement that: \begin{align} F_1 = F_2 &\Leftrightarrow \forall x, F_1(x) = F_2(x) \end{align}

Since we know that $F_1, F_2$ are algebra morphisms, we can do better, using the fact that $\operatorname{lift}$ is a one-to-one mapping!

\begin{align} F_1 = F_2 &\Leftrightarrow \operatorname{lift}^{-1}[F_1] = \operatorname{lift}^{-1}[F_2] \\ &\Leftrightarrow F_1 \circ \iota = F_2 \circ \iota \\ &\Leftrightarrow \forall \vec{v}, F_1(\iota(\vec{v})) = F_2(\iota(\vec{v})) \end{align}


To show two algebra morphisms from a geometric algebra agree,
it suffices to show they agree on the vectors

Applying the universal property

  1. Choose a construction $A$

  2. Show that $A$ is an $R$-algebra

  3. Choose a linear map $f : V \lin{R} A$

  4. Prove that for all $\vec{v}$, $f(\vec{v})^2 = \Qv 1$

  5. Obtain $F = \operatorname{lift}[f]$

Applying the universal propertyGrade involution

1. Choose a construction $A$

Let $A := \mathcal{G}(V, Q)$

2. Show that $A$ is an $R$-algebra

We know this already

3. Choose a linear map $f : V \lin{R} A$

Let $f := \vec{v} \mapsto \iota(\vec{-v})$

4. Prove that for all $\vec{v}$, $f(\vec{v})^2 = \Qv 1$
\begin{align} f(\vec{v})^2 &= \iota(\vec{-v})^2 \\ &= (-\iota(\vec{v}))^2 \text{ (by linearity)} \\ &= \iota(\vec{v})^2 \\ &= \Qv 1 \text{ (the defining property of $\iota$)} \end{align}
5. Obtain $F = \operatorname{lift}[f]$
$$\hat x = \operatorname{lift}[f](x)$$

Check with $x = \iota(\vec{u})\times\iota(\vec{v})\times\iota(\vec{w})$:

\begin{align} \hat x &= \operatorname{lift}[f](\iota(\vec{u})\times\iota(\vec{v})\times\iota(\vec{w})) \\ &= f(\vec{u})\times f(\vec{v})\times f(\vec{w}) \\ &= \iota(\vec{-u}) \times \iota(\vec{-v}) \times \iota(\vec{-w}) \\ &= -\iota(\vec{u}) \times \iota(\vec{v}) \times \iota(\vec{w}) \end{align}

Involute of a 3-vector is its negation.

Applying the universal propertyGrade reversal

1. Choose a construction $A$

Define the multiplicative opposite $A^\mathrm{op}$, which as a module is isomorphic to $A$:

\begin{align} \operatorname{op} &: A \lin{R} A^\mathrm{op}, & \operatorname{op}^{-1} &: A^\mathrm{op} \lin{R} A \end{align}
but has a reversed multiplication rule
\begin{align} \operatorname{op} 1 &= 1, & \operatorname{op}(x \times y) &= \operatorname{op} y \times \operatorname{op} x \\ \operatorname{op}^{-1} 1 &= 1, & \operatorname{op}^{-1}(x \times y) &= \operatorname{op}^{-1} y \times \operatorname{op}^{-1} x \end{align}

Let $A := \mathcal{G}(V, Q)^\mathrm{op}$.

2. Show that $A$ is an $R$-algebra

Can be shown straightforwardly

3. Choose a linear map $f : V \lin{R} A$

Let $f := \vec{v} \mapsto \operatorname{op} \iota(\vec{v})$

4. Prove that for all $\vec{v}$, $f(\vec{v})^2 = \Qv 1$
\begin{align} f(\vec{v})^2 &= (\operatorname{op} \iota(\vec{v}))^2 \\ &= \operatorname{op} \iota(\vec{v})^2 & \text{ (from the definition of $\times$ on $A^\mathrm{op}$)} \\ &= \operatorname{op} (\Qv 1) & \text{ (the defining property of $\iota$)} \\ &= \Qv(\operatorname{op} 1) & \text{ (from the definition of $\sca{r}x$ on $A^\mathrm{op}$)}\\ &= \Qv 1 & \text{ (from the definition of $1$ on $A^\mathrm{op}$)} \end{align}
5. Obtain $F = \operatorname{lift}[f]$
$$\tilde x = \operatorname{op}^{-1}(\operatorname{lift}[f](x))$$

Check with $x = \iota(\vec{u})\times\iota(\vec{v})\times\iota(\vec{w})$:

\begin{align} \tilde x &= \operatorname{op}^{-1}(\operatorname{lift}[f](\iota(\vec{u})\times\iota(\vec{v})\times\iota(\vec{w}))) \\ &= \operatorname{op}^{-1}( f(\vec{u})\times f(\vec{v})\times f(\vec{w})) \\ &= \operatorname{op}^{-1}( \operatorname{op}\iota(\vec{u}) \times \operatorname{op}\iota(\vec{v}) \times \operatorname{op}\iota(\vec{w})) \\ &= \operatorname{op}^{-1}(\operatorname{op}( \iota(\vec{w}) \times \iota(\vec{v}) \times \iota(\vec{u}))) \\ &= \iota(\vec{w}) \times \iota(\vec{v}) \times \iota(\vec{u}) \end{align}

Reversion flips the
order of the vectors.

Applying the universal propertyAn induction rule

Let $P(z)$ be some statement about all multivectors $z$. We wish to show it is true for all multivectors.

Let's build an induction rule, which says to prove $h : P(z)$ it suffices to show:

\begin{align} h_r &: \forall \sca{r}, P(\sca{r}1), & h_\iota &: \forall \vec{v}, P(\iota(\vec{v})), & h_{+} &: \forall x, \forall y, P(x), P(y) \implies P(x + y), & h_{\times} &: \forall x, \forall y, P(x), P(y) \implies P(x \times y). \end{align}

The $\Rightarrow$ in $h_{+}$ and $h_{\times}$ can be thought of as functions taking two proofs and producing a third.

Example: Using such a rule to prove $\forall z, \tilde{\tilde{z}} = z$

$P(x)$$\tilde{\tilde{z}} = z$, where $\tilde z = \operatorname{op}^{-1} \left(\operatorname{lift}[f](z)\right), f = \vec{v} \mapsto \operatorname{op} \iota(\vec{v})$
$h_r : \forall \sca{r}, P(\sca{r}1)$ $\widetilde{\widetilde{\sca{r}1}} = \widetilde{\sca{r}\widetilde{1}} = \sca{r}\tilde{\tilde{1}} = \sca{r}1$ using linearity of $\operatorname{op}$ and $\operatorname{lift}[f]$
$h_\iota: \forall \vec{v}, P(\iota(\vec{v}))$ $\widetilde{\widetilde{\iota(\vec{v})}} = \widetilde{\iota(\vec{v})} = \iota(\vec{v})$ using $\operatorname{lift}[f](\iota(\vec{v})) = \operatorname{op} \iota(\vec{v})$
$h_{+}: \forall x, \forall y, P(x), P(y) \Rightarrow P(x + y)$ $\begin{aligned}\widetilde{\widetilde{x + y}} = \widetilde{\widetilde{x} + \tilde{y}} &= \tilde{\tilde{x}} + \tilde{\tilde{y}} \\ &= x + y\text { using $h_x : P(x)$ and $h_y : P(y)$}\end{aligned}$
$h_{\times}: \forall x, \forall y, P(x), P(y) \Rightarrow P(x \times y)$ $\begin{aligned}\widetilde{\widetilde{x \times y}} = \widetilde{\tilde{y} \times \tilde{x}} &= \tilde{\tilde{x}} \times \tilde{\tilde{y}} \\ &= x \times y\text { using $h_x : P(x)$ and $h_y : P(y)$}\end{aligned}$
1. Choose a construction $A$

Let $A := \pair{x : \mathcal{G}(V, Q)}{h : P(x)}$, pairs consisting of a multivector and a proof that it satisfies $P$.

2. Show that $A$ is an $R$-algebra
\begin{align} 0 &:= \pair{0}{\left.h_{r}\right|_{r=\sca{0}}} & \pair{x}{h_x} + \pair{y}{h_y} &:= \pair{x + y}{h_{+}(h_x, h_y)}\\ 1 &:= \pair{1}{\left.h_{r}\right|_{r=\sca{1}}} & \pair{x}{h_x} \times \pair{y}{h_y} &:= \pair{x \times y}{h_{\times}(h_x, h_y)} \\ && \sca{r}\pair{x}{h_x} &:= \pair{\sca{r}x}{h_{\times}(h_r(\sca{r}), h_x)} \end{align}

Associativity, distributivity, … follow trivially if we assume proof irrelevance, that $x = y \implies \pair{x}{h_x} = \pair{y}{h_y}$.

3. Choose a linear map $f : V \lin{R} A$

Let $f := \vec{v} \mapsto \pair{\iota(\vec{v})}{h_{\iota}(\vec{v})}$, which is linear by inspection.

4. Prove that for all $\vec{v}$, $f(\vec{v})^2 = \Qv 1$
\begin{align} f(v)^2 &= \pair{\iota(\vec{v})}{\ldots}^2 \\ &= \pair{\iota(\vec{v})^2}{\ldots} & \text{ (from the definition of $\times$)} \\ &= \pair{\Qv 1}{\ldots} & \text{ (the defining property of $\iota$)} \\ &= \Qv \pair{1}{\ldots} & \text{ (from the definition of $\sca{r}x$)} \\ &= \Qv 1 & \text{ (from the definition of $1$)}\end{align}
5. Obtain $F = \operatorname{lift}[f]$

Let $\operatorname{value} : A \alg{R} \mathcal{G}(V, Q) = \pair{z}{h_z} \mapsto z$.

\begin{align} \operatorname{value} (\operatorname{lift}[f](\iota(\vec{v}))) &= \operatorname{value} (f(\vec{v})) \\ &= \operatorname{value}(\!\pair{\iota(\vec{v})}{h_{\iota}(\vec{v})}\!) \\ &= \iota(\vec{v}) \\ \implies \operatorname{value} (\operatorname{lift}[f](z)) &= z & \qquad\qquad\mathllap{\text{ (by extensionality)}}\\ \implies \operatorname{lift}[f](z) &= \pair{z}{h_z} & \mathllap{\text{ (by the definition of $\operatorname{value}$)}} \end{align}
$h_z : P(z)$ is our result.

Applying the universal propertyA summary

Using the universal property largely comes down to a clever choice of $A$ and $f$.

The space of clever constructions is unbounded, the universal property doesn't help you find the one that has the properties you need!

Some more involved applications

Splitting into even- and odd-graded parts
Choose $A = \pair{\pair{e : \mathcal{G}(V, Q)}{h_e : \mathrm{even}(e)}}{\pair{o : \mathcal{G}(V, Q)}{h_o : \mathrm{odd}(o)}}$. Showing this is an algebra is tedious!
Choose $f = \vec{v} \mapsto \pair{0}{\pair{\iota(\vec{v})}{\text{trivial}}}$
Splitting into the usual grades

Choose $A$ as the exterior algebra $\bigwedge(V)$? Can we choose a basis-free $f$? Does it need $R$ to be a field so that we can compute $\frac{1}{n!}$? How do we get back from $\bigwedge(V)$ to $\mathcal(V, Q)$?

Some ideas in:

Wedge product
Use a similar map to the above, then compute the product in $\bigwedge(V)$?

Applying the universal propertyDude, there's my basis!

1. Choose a construction $A$

Use a more convenient model of a geometric algebra that depends on a basis, like $A = \sca{a}1 + \sca{a_1}e_1 + \sca{a_2}e_2 + \sca{a_{12}}e_{12}$

2. Show that $A$ is an $R$-algebra

Our model should come with this

3. Choose a linear map $f : V \lin{R} A$

Let $f$ be the $\iota$ in our model; $f(\sca{a_1}\vec{e_1} + \sca{a_2}\vec{e_2}) = \sca{a_1}e_1 + \sca{a_2}e_2$

4. Prove that for all $v$, $f(\vec{v})^2 = \Qv 1$

Our model should satisfy this

5. Obtain $F = \operatorname{lift}[f]$

This is the function that sends any multivector in the abstract $\mathcal{G}(V, Q)$ to our alternate model $A$

Now we can do what we like in our alternate model.

Use the universal property of the alternate model $\operatorname{lift}_A$ in the same way to get back to the abstract $\mathcal{G}(V, Q)$; $$\operatorname{lift}_A[f](\sca{a}1 + \sca{a_1}e_1 + \sca{a_2}e_2 + \sca{a_{12}}e_{12}) = \sca{a}1 + \sca{a_1}f(\vec{e_1}) + \sca{a_2}f(\vec{e_2}) + \sca{a_{12}}f(\vec{e_1})\times f(\vec{e_2})$$

And then?

And then?Other universal properties

Geometric algebra isn't the only thing with a universal property:

$\mathcal{G}(V, Q)$
$f : V \lin{R} A$ where $f(\vec{v})^2 = \sca{Q(}v\sca{)}1$
$F : \mathcal{G}(V, Q) \alg{R} A$
$f : V \lin{R} A$ where $f(\vec{v})^2 = 0$
$F : \bigwedge(V) \alg{R} A$
$f : V \lin{R} A$
$F : T(V) \alg{R} A$

The techniques we saw earlier transfer to the tensor and exterior algebras too.

And then?Why we care

  • The universal property provides an unusual framework for understanding GA, with analogies elsewhere in mathematics.
  • The universal property lets us work in highly generalized cases where no basis can be reached for.

Why care about highly generalized cases?

The road that led me here: defining GA in a theorem proving language. The universal property there:

                  -- here's where we need the abstract algebra
                  variables {R M A : Type*}
                  variables [comm_ring R] [add_comm_group M] [module R M] [semiring A] [algebra R A]
                    -- this is the same as the `lift` in this presentation
                    def lift (Q : quadratic_form R M) :
                      {f : M →ₗ[R] A // ∀ m, f m * f m = Q m • 1}
                      (clifford_algebra Q →ₐ[R] A) := sorry
                    -- this is the statement that `lift[f](ι(v)) = f(v)`
                    @[simp] theorem lift_ι_apply {Q : quadratic_form R M}
                      (f : M →ₗ[R] A) (hf : ∀ m, f m * f m = Q m • 1) (m : M) :
                      lift Q ⟨f, hf⟩ (ι Q m) = f m := sorry

If you're contributing a formalization to a coherent library of mathematics, you want it to work for every paper about Clifford algebras, not just the ones that assume a basis!

The library in question: Lean's Mathlib, with almost 70k theorems!

And then?And then?

These slides: eric-wieser.github.io/brno-2021

A universal property-based formalization of GA in Lean: github.com/pygae/lean-ga

A paper summarizing that formalization: arXiv:2110.03551 [cs.LO]

Getting started with Lean: leanprover-community.github.io/learn