Eric Wieser
Cambridge University Engineering Department
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!
If $V$ has a basis $\vec{e_i}$, then $\mathcal{G}(V)$ usually has both of the following bases:
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)
Algorithms fall into one of three categories:
The choice of basis affects the result
The computation needs a basis, but the outcome isn't affected by the choice.
The entire computation can be done without reference to a basis
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 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}$,
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}}$:
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$.
freelymultiplied.
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$
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:
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,
We say $R$ is a ring
if it has $0$,$+$,$-$,$1$,$\times$, and they satisfy some basic rules of arithmetic:
Multiplication is not necessarily commutative1 or cancellative2!
If we add an inverse (${}^{-1}$), this is a division ring
or field
when also commutative.
Examples:
We say $M$ is an $R$-module
if it has $0$, $+$, and scalar multiplication by elements of a ring $R$ satisfying:
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!
Examples:
We say that $A$ is an $R$-algebra
if it is both a ring and an $R$-module, and additionally satisfies:
Examples:
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$.
Examples:
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$.
Examples:
sandwich productof a fixed rotor on a multivector.
For any choice of an $R$-algebra $A$, there is one-to-one correspondence we'll call $\operatorname{lift}$ between
$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]$.
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$.
| $\operatorname{lift}[f_2](\iota(\vec{v})) = f_2(\vec{v})$ | $\operatorname{lift}[f]$ is like the outermorphismof $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. |
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}Intuition:
To show two algebra morphisms from a geometric algebra agree,.
it suffices to show they agree on the vectors
Choose a construction $A$
Show that $A$ is an $R$-algebra
Choose a linear map $f : V \lin{R} A$
Prove that for all $\vec{v}$, $f(\vec{v})^2 = \Qv 1$
Obtain $F = \operatorname{lift}[f]$
Let $A := \mathcal{G}(V, Q)$
We know this already
Let $f := \vec{v} \mapsto \iota(\vec{-v})$
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.
Define the multiplicative opposite $A^\mathrm{op}$, which as a module is isomorphic to $A$:
Let $A := \mathcal{G}(V, Q)^\mathrm{op}$.
Can be shown straightforwardly
Let $f := \vec{v} \mapsto \operatorname{op} \iota(\vec{v})$
Check with $x = \iota(\vec{u})\times\iota(\vec{v})\times\iota(\vec{w})$:
✔ Reversion flips the
order of the vectors.
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:
The $\Rightarrow$ in $h_{+}$ and $h_{\times}$ can be thought of as functions taking two proofs and producing a third.
| $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}$ |
Let $A := \pair{x : \mathcal{G}(V, Q)}{h : P(x)}$, pairs consisting of a multivector and a proof that it satisfies $P$.
Associativity, distributivity, … follow trivially if we assume proof irrelevance, that $x = y \implies \pair{x}{h_x} = \pair{y}{h_y}$.
Let $f := \vec{v} \mapsto \pair{\iota(\vec{v})}{h_{\iota}(\vec{v})}$, which is linear by inspection.
Let $\operatorname{value} : A \alg{R} \mathcal{G}(V, Q) = \pair{z}{h_z} \mapsto z$.
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!
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:
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}$
Our model should come with this
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$
Our model should satisfy this
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})$$
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$
$\Rightarrow$
$F : \mathcal{G}(V, Q) \alg{R} A$
|
|---|---|
| $\bigwedge(V)$ |
$f : V \lin{R} A$
where $f(\vec{v})^2 = 0$
$\Rightarrow$
$F : \bigwedge(V) \alg{R} A$
|
| $T(V)$ |
$f : V \lin{R} A$
$\Rightarrow$
$F : T(V) \alg{R} A$
|
The techniques we saw earlier transfer to the tensor and exterior algebras too.
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!
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