APPLICATIONS OF GEOMETRIC ALGEBRA​

# Computing with the universal properties of the Clifford algebra and the even subalgebra

Eric Wieser, Joan Lasenby
Cambridge University Engineering Department

slides: eric-wieser.github.io/icacga-2022 2022-10-04

### IntroductionNotational preliminaries

$r : \mathbb{R}$
Let $x$ be a real number, e.g. $\,r \coloneqq \pi$
$p : V \times W$
Let $p$ be a pair of elements from $V$ and $W$, e.g. $\,p \coloneqq (v, w)$
$f : V \to V$
Let $f$ be a function from $V$ to itself, e.g. $\,f \coloneqq v \mapsto 2v$
$g : A \to A \to A$
Let $g$ be a binary function of $A$, e.g. $\,g \coloneqq x \mapsto (y \mapsto x + y)$
$\mathcal{G}(\mathbb{R}^{p,q,r})$ and shorthands $\mathcal{G}(\mathbb{R}^{p,q})$, $\mathcal{G}(\mathbb{R}^{p})$
The geometric algebra over the real-vector space spanned by the orthogonal basis $\{\vec{e^{\mathrlap{+}}_1}, \dotsc, \vec{e^{\mathrlap{+}}_p}, \vec{e^{\mathrlap{-}}_1}, \dotsc, \vec{e^{\mathrlap{-}}_q}, \vec{e^{0}_1}, \dotsc, \vec{e^{0}_r}\}$, with $\vec{e^{\mathrlap{+}}_i} \cdot \vec{e^{\mathrlap{+}}_i} = \sca{1}$, $\vec{e^{\mathrlap{-}}_i} \cdot \vec{e^{\mathrlap{-}}_i} = \sca{-1}$, and $\vec{e^{0}_i} \cdot \vec{e^{0}_i} = \sca{0}$.
$\GVQ$

The geometric algebra over an $R$-vector space $V$, with quadratic form $Q : V \to R$.

For $\mathbb{R}^{p,q,r}$, $\Qof{\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}} = {\sum_{i=1}^p \sca{{(a^{+}_i)}^2} - \sum_{i=1}^q \sca{{(a^{-}_i)}^2}}$

### IntroductionThe isomorphism with the even subalgebra, $\mathcal{G}^{+}$

$\mathbb{C} \cong \mathcal{G}(\mathbb{R}^{0,1}) \cong \mathcal{G}^{+}(\mathbb{R}^{0,2}), \qquad \mathbb{H} \cong \mathcal{G}(\mathbb{R}^{0,2}) \cong \mathcal{G}^{+}(\mathbb{R}^{0,3})$

Add a new basis vector $e_{-}^2 = -1$, build the (known) map

$\begin{CD} 1 @. @. e_1 @. e_2 @. e_3 @. @. e_{12} @. e_{23} @. e_{31} @. @. e_{123} @. : @. \mathcal{G}(\mathbb{R}^3) \\ @VVV @. @VVV @VVV @VVV @. @VVV @VVV @VVV @. @VVV @. @VVFV \\ 1 @. @. e_1\boldsymbol{e_{-}}@. e_2\boldsymbol{e_{-}} @. e_3\boldsymbol{e_{-}} @. @. e_{12} @. e_{23} @. e_{31} @. @. e_{123}\boldsymbol{e_{-}} @. : @. \mathcal{G}^{+}(\mathbb{R}^{3,1}) \end{CD}$

bijective , linear , basis-independent ?

Software implementation is certainly not coordinate-free!


def to_even(x: g3.MultiVector) -> g3p1.MultiVector:
[c,   c1, c2, c3,   c12, c23, c31,   c123] = x.value
return g3p1.MultiVector(
[c,   0, 0, 0, 0,   c1, c2, c3, c12, c23, c31,
0, 0, 0, 0,   c123])


def from_even(x: g3p1.MultiVector) -> g3.MultiVector:
[c,   _, _, _, _,   c1e, c2e, c3e, c12, c23, c31,
_, _, _, _,   c123e] = x.value
return g3.MultiVector(
[c,   c1e, c2e, c3e,   c12, c23, c31,   c123e])


### IntroductionThe isomorphism with the even subalgebra, $\mathcal{G}^{+}$

What about the general case, $\GVQ \cong \mathcal{G}^{+}(V \oplus R, Q')$?

(with $Q'(v + re_{-}) = Q(v) - r^2$)

$\begin{CD} 1 @. @. v @. @. uv @. @. uvw @. @. \cdots @. : @. \GVQ \\ @VVV @. @VVV @. @VVV @. @VVV @. @. @. @VVFV \\ 1 @. @. v\boldsymbol{e_{-}}@. @. uv @. @. uvw\boldsymbol{e_{-}} @. @. \cdots @. : @. \mathcal{G}^{+}(V \oplus R, Q') \end{CD}$

Is this well-defined for all $Q$?

Can we compute this without invoking a basis?

### IntroductionOutline

Using $\GVQ \cong \mathcal{G}^{+}(V \oplus R, Q')$ as a motivating example, we will:

Explore the universal property of $\GVQ$
This provides a tool for generalizing the forward direction $\GVQ \to \mathcal{G}^{+}(V \oplus R, Q')$
Explore recursion techniques from function programming
These can be translated to techniques for using the universal property
Construct a universal property for $\mathcal{G}^{+}(V, Q)$
This is the tool we need to generalize the reverse direction $\mathcal{G}^{+}(V \oplus R, Q') \to \GVQ$
Discuss relevance to formalization
Things omitted from these slides are available in excruciating software-verified detail!

### The universal property of $\GVQ$Informally

Given a function $f : V \to A$, construct $F : \GVQ \to A$ as

\begin{align*} F(1) &\coloneqq 1 \\ F(v : V) &\coloneqq f(v) \end{align*}
extended by
\begin{align*} F(x + y) &\coloneqq F(x) + F(y) \\ F(xy) &\coloneqq f(x)f(y) \end{align*}

Similar to the outermorphism which builds
$F : \bigwedge V \to \bigwedge W$ from $f : V \to W$, but with $xy$ not $x \wedge y$.

Example: $F(1 + 2e_1 + 3e_{12}) = 1 + 2f(e_1) + 3f(e_1)f(e_2)$

Not well-defined on all $f$, consider $f = v \mapsto 0$:
$1 \eqqcolon F(1) = F(e_1e_1) \coloneqq F(e_1)F(e_1) = f(e_1)f(e_1) = 0$ (!)

### The universal property of $\GVQ$Formally

For any choice of an $R$-algebra $A$, there is 1:1 correspondence between

$f : V \lin{R} A$

$f(\vec{v})^2 = \sca{Q(}v\sca{)}1$

and
$F : \mathcal{G}(V, Q) \alg{R} A$

\begin{align*} F &= \operatorname{lift}[f] \\ f &= \operatorname{lift}^{-1}[F] \\ &= u \mapsto F(\iota(u))\\ &= u \mapsto F(u) \end{align*}

### The universal property of $\GVQ$Applied to our motivating example, $\mathcal{G}(\ ) \cong \mathcal{G}^{+}(\ )$

How do we compute $\begin{CD} 1 @. @. v @. @. uv @. @. uvw @. @. \cdots @. : @. \GVQ \\ @VVV @. @VVV @. @VVV @. @VVV @. @. @. @VVFV \\ 1 @. @. v\boldsymbol{e_{-}}@. @. uv @. @. uvw\boldsymbol{e_{-}} @. @. \cdots @. : @. \mathcal{G}^{+}(V \oplus R, Q') \end{CD}$ ?

Would applying the universal property with $f \coloneqq v \mapsto ve_{-}$ work?

$F(uv) = f(u)f(v) = ue_{-}ve_{-} = -ue_{-}^2v = -u(-1)v = uv$

Are we allowed to?

$f$ is linear ,

$f(v)f(v) = vv = Q(V)$

#### Result

$\operatorname{to\_even} : \GVQ \alg{R} \mathcal{G}^{+}(V\oplus R, Q') \coloneqq \operatorname{lift}[f]$

### The universal property of $\GVQ$… as a universal interface

If a software library libA implements the universal property:


def libA.g3_universal_property(f, x: libA.g3.MultiVector):
""" Evaluate $\operatorname{lift}[f](x)$ """
e1, e2, e3 = [1, 0, 0], [0, 1, 0], [0, 0, 1]
[c,   c1, c2, c3,   c12, c12, c31,   c123] = x.value
return (x + c1*f(e1)        + c2*f(e2)        + c3*f(e3)
+ c12*f(e1)*f(e2) + c23*f(e2)*f(e3) + c31*f(e3)*f(e1) + c123*f(e1)*f(e2)*f(e3))

Then we can implement to_even between libraries as:

def to_even_f(v: V) -> libB.g3p1.EvenMultiVector:
return libB.g3p1.EvenMultiVector.iota((v, 0), (0, 1))  # $ve_{-}$

def to_even(mv: libA.g3.MultiVector) -> libB.g3p1.EvenMultiVector:
return libA.g3.universal_property(to_even_f, mv)

Note: implemention is now coordinate-free!
Or even just translate directly between libraries with $f = v \mapsto \iota_\mathtt{B}(v)$:

def to_even(mv: libA.g3.MultiVector) -> libB.g3.MultiVector:
return libA.g3.universal_property(libB.MultiVector.iota, mv)

(since mathematically, $\operatorname{lift}[\iota](x) = x$)

### The universal property of $\GVQ$Building other basic operators

Grade involution, $\hat x$

Let $f : V \to \GVQ \coloneqq v \mapsto -v$.

$f(v)^2 = (-v)^2 = v^2 = Q(v)$

Then $\hat x \coloneqq \operatorname{lift}[f](x)$.

Grade reversal, $\tilde x$

Let $A^\mathrm{op}$ be the opposite algebra of $A$, where $\operatorname{op} (xy) = (\operatorname{op} y)(\operatorname{op} x)$ and $\operatorname{op}c = c$.

Let $f : V \to \htmlData{fragment-index=3}{\htmlClass{fragment highlight-blue}{\GVQ^\mathrm{op}}} \coloneqq v \mapsto \operatorname{op} v$.

\begin{aligned}f(v)^2 &= (\operatorname{op} v)^2 = \operatorname{op} (v^2) \\ &= \operatorname{op} (Q(v)) = Q(v)\,\htmlClass{c-success}{✔}\end{aligned}

Then $\tilde x = \htmlData{fragment-index=3}{\htmlClass{fragment highlight-teal}{\operatorname{op}^{-1}}}(\operatorname{lift}[f](x))$.

The key trick; choose a clever algebra, and suitable post-processing

## Recursors

A function can be defined on a list by defining it:

on $[~]$, the empty list

on $a :: l$ given its value on $l$

(Note: $[a, b, c] = a :: b :: c :: [~]$ by definition)

\begin{align*} \operatorname{sum} : \operatorname{list} R &\to R \\ \operatorname{sum}([~]) &\coloneqq 0 \\ \operatorname{sum}(a :: l) &\coloneqq a + \htmlClass{fragment highlight-blue fragment-index-3}{\operatorname{sum}(l)} \end{align*}

#### Lean


def sum : list R → R
| []       := 0
| (a :: l) := a + sum l



sum :: [R] -> R
sum []     = 0
sum (x:xs) = x + sum xs


### RecursorsExtra inputs

Let's define acc([a, b, c]) = [0, a, a + b, a + b + c]:

\begin{alignat*}{3} \operatorname{acc\_from} : \operatorname{list} R &\to \emblue{R} &&\emblue{\to \operatorname{list} R} \\ \operatorname{acc\_from}([~]) &\coloneqq a &&\mapsto [a] \\ \operatorname{acc\_from}(b :: l) &\coloneqq a &&\mapsto a :: \emblue{\operatorname{acc\_from}(l)}(a + b) \end{alignat*}

\begin{alignat*}{3} \operatorname{acc} &: &\operatorname{list} R &\to \operatorname{list} R \\ \operatorname{acc} &\coloneqq &l &\mapsto \operatorname{acc\_from}(l)(0) \end{alignat*}

#### Lean


def acc_from : list R → R → list R
| []       := λ a, [a]
| (b :: l) := λ a, a :: acc_from l (a + b)


def acc : list R → list R :=
λ l, acc_from l 0


### RecursorsExtra outputs

Let's define rev_acc([a, b, c]) = [a+b+c, b+c, c, 0]

\begin{alignat*}{5} \operatorname{rev\_acc_{aux}} : \operatorname{list} R &\to{}& (\emblue{R}{}\mkern9mu&\mkern-9mu\emblue{\times\operatorname{list} R})\\ \operatorname{rev\_acc_{aux}}([~]) &\coloneqq{}& ( 0&, [~]) \\ \operatorname{rev\_acc_{aux}}(a :: l) &\coloneqq{}& (a + b&, b :: l') \text{ where } (b&, l') \coloneqq \operatorname{rev\_acc_{aux}}(l) \end{alignat*}
\begin{alignat*}{3} \operatorname{rev\_acc} &: &\operatorname{list} R &\to \operatorname{list} R \\ \operatorname{rev\_acc} &\coloneqq & l &\mapsto a :: l' \text{ where } (a, l') \coloneqq \operatorname{rev\_acc_{aux}}(l) \end{alignat*}

#### Lean


def rev_acc_aux : list R → R × list R
| []       := (0, [])
| (a :: l) := let (b, l') := rev_acc_aux l
in (a + b, b :: l')


def rev_acc : list R → list R :=
λ l, let (b, l') := rev_acc_aux l
in b :: l'


### RecursorsRecap

Clever output types enable more sophisticated recursion schemes:

Functions ($S \to \cdot$)
Push state $S$ into inner recursors. Initialize with the initial state $s_0 : S$.
Products ($S \times \cdot$) a.k.a. direct sums ($S \oplus \cdot$)
Pull state out of inner recursors. The final state $S_n$ is available for post-processing.

These tricks are composable; the output type $S \to (S \times \cdot)$
lets us evolve a state $s_i : S$ throughout the recursion.

### RecursorsExtra inputs with the universal property

The space of functions $W \to W$ do not form an $R$-algebra…
…but the space of $R$-linear maps $W \to W$ (aka $\mathrm{End}_R(W)$) do! Define

$$1 \coloneqq (w \mapsto w),\qquad fg \coloneqq (w \mapsto f(g(w)))$$

Let's apply $\operatorname{lift}$ to $f : V \to \mathrm{End}_R(W)$.
The $f(v)f(v) = Q(v)1$ requirement becomes $f(v, f(v, w)) = Q(v)w$.

#### Result

\begin{alignat*}{5} \operatorname{lift}[f](&&v : V, w_0) &= f(v, w_0) \\ \operatorname{lift}[f](&&1, w_0) &= w_0 \\ \operatorname{lift}[f](&&xy, w_0) &= \operatorname{lift}[f](x, \operatorname{lift}[f](y, w_0)) \\ \end{alignat*}

### RecursorsExtra inputs with the universal property

#### Result

\begin{alignat*}{5} \operatorname{lift}[f](&&v : V, w_0) &= f(v, w_0) \\ \operatorname{lift}[f](&&1, w_0) &= w_0 \\ \operatorname{lift}[f](&&xy, w_0) &= \operatorname{lift}[f](x, \operatorname{lift}[f](y, w_0)) \\ \end{alignat*}

For example,

\begin{align*} \operatorname{lift}[f](e_{123}, w_0) &= f(e_1, f(e_2, f(e_3, w_0))) \\ \operatorname{lift}[f](2 + 3e_{12}, w_0) &= 2x_0 + 3f(e_1, f(e_2, w_0)) \end{align*}

### The universal property of $\GVQe$Informally

Given a function $f : V \to V \to A$, construct $F : \GVQe \to A$ as

\begin{align*} F(1) &\coloneqq 1 \\ F(uv) &\coloneqq f(u, v) \end{align*}
extended by
\begin{align*} F(x + y) &\coloneqq F(x) + F(y) \\ F(xy) &\coloneqq f(x)f(y) \end{align*}

Example:
$F(1 + 3e_{12} + 5e_{1234}) = 1 + 3f(e_1, e_2) + 5f(e_1, e_2)f(e_3, e_4)$

Not well-defined on all $f$, consider $f = u \mapsto v \mapsto 0$:
$1 \eqqcolon F(1) = F(e_1e_1) \coloneqq f(e_1, e_1) = 0$

### The universal property of $\GVQe$Formally

For any choice of an $R$-algebra $A$, there is 1:1 correspondence between

$f : V \lin{R} V \lin{R} A$

\begin{align*} f(v, v)^2 &= \sca{Q(}v\sca{)}1 \\ f(v_1, v_2)f(v_2, v_3) &= \sca{Q(}v_2\sca{)}f(v_1, v_3) \end{align*}

and

$F : \GVQe \alg{R} A$

\begin{align*} F &= \operatorname{lift}^{+}[f] \\ f &= \operatorname{lift}^{-1}[F] \\ &= u \mapsto v \mapsto F(\iota^{+}(u, v))\\ &= u \mapsto v \mapsto F(uv) \end{align*}

### The universal property of $\GVQe$Constructed from the universal property of $\GVQ$

We want:
$$\operatorname{lift}^{+}[f](1 + e_{12} + e_{1234}) = 1 + f(e_1, e_2) + f(e_1, e_2)f(e_3, e_4)$$

For a suitable $g : V \to \mathrm{End}_R(W)$ and $w_0 : W$, we saw that:
$\begin{split} \operatorname{lift}[g](1 + e_{12} + e_{1234}, w_0) = w_0 &+ g(e_1, g(e_2, w_0)) \\&+ g(e_1, g(e_2, g(e_3, g(e_4, w_0)))) \end{split}$

If we can make $h(g(v_1, g(v_2, w)) = f(v_1, v_2)h(w)$ and $h(w_0) = 1$, then

$$\htmlData{id=lift-def-lhs}{\operatorname{lift}^{+}[f](x) \coloneqq} h(\htmlData{id=lift-def-rhs-1}{\operatorname{lift}[g](x,} w_0 \htmlData{id=lift-def-lhs-2}{)})$$

Solve for $W$ and $h : W \to A$ and $w_0 : W$ and $g : V \to \mathrm{End}_R(W)$!

### The universal property of $\GVQe$Constructed from the universal property of $\GVQ$

$$\htmlData{id=lift-def-lhs}{\operatorname{lift}^{+}[f](x) \coloneqq} h(\htmlData{id=lift-def-rhs-1}{\operatorname{lift}[g](x,} w_0 \htmlData{id=lift-def-lhs-2}{)})$$

Solve $h(\htmlData{id=constraints-lhs-1}{g(v_1, g(v_2,} w\htmlData{id=constraints-lhs-2}{))} = \htmlData{id=constraints-rhs}{f(v_1, v_2)}h(w)$ and $h(w_0) = 1$
for $W$ and $h : W \to A$ and $w_0 : W$ and $g : V \to \mathrm{End}_R(W)$

Inspired by the recursor slides, try
$$W \coloneqq A \oplus S,\qquad h \coloneqq (a, s) \mapsto a, \qquad w_0 \coloneqq (1, 0)$$

### The universal property of $\GVQe$Constructed from the universal property of $\GVQ$

$$( \htmlData{id=lift-def-lhs}{\operatorname{lift}^{+}[f](x)}, \dotsc) \coloneqq \htmlData{id=lift-def-rhs-1}{\operatorname{lift}[g](x,} (1, 0) \htmlData{id=lift-def-lhs-2}{)}$$

Solve $\htmlData{id=constraints-lhs-1}{g(v_1, g(v_2,} (a, s)\htmlData{id=constraints-lhs-2}{))} = (\htmlData{id=constraints-rhs}{f(v_1, v_2)}a, \dotsc)$
for $S$ and $g : V \to \mathrm{End}_R(A \oplus S)$

If $S$ holds half-applied versions of $f$, we can define

\begin{align*} g : V \to \mathrm{End}_R(A \oplus S) &\coloneqq v \mapsto (a, s) \mapsto (s(v), w \mapsto f(w, v) a) \\ \implies g(v_1, g(v_2, (a, s))) &= g(v_1, (s(v_2), w \mapsto f(w, v_2) a)) \\ &= (f(v_1, v_2) a, w \mapsto f(w, v_1) s(v_2)))\,\htmlClass{c-success}{✔}\end{align*}

### The universal property of $\GVQe$Constructed from the universal property of $\GVQ$

$$(\operatorname{lift}^{+}[f](x), \dotsc) \coloneqq \operatorname{lift}[g](x, (1, 0))$$

Let $S$ hold half-applied versions of $f$ (roughly* $S \coloneqq V \to A$)

\begin{align*} g : V \to \mathrm{End}_R(A \oplus S) &\coloneqq v \mapsto (a, s) \mapsto (s(v), w \mapsto f(w, v) a) \\ \implies g(v_1, g(v_2, (a, s))) &= g(v_1, (s(v_2), w \mapsto f(w, v_2) a)) \\ &= (f(v_1, v_2) a, w \mapsto f(w, v_1) s(v_2)))\phantom{\,\htmlClass{c-success}{✔}}\end{align*}

For $\operatorname{lift}[g]$ to be valid, we need the $*$ in:

\begin{alignat*}{3} g(v, g(v, (a, s))) &= (f(v, v) a, {}&w &\mapsto f(w, v) s(v))) \\ &\stackrel{\smash{*}}{=}(Q(v)a, {}&w &\mapsto Q(v)s(w)) = Q(v)(a, s)\end{alignat*}

Need $f(v, v) = \sca{Q(}v\sca{)}1$ (easy) and $f(v_1, v_2)f(v_2, v_3) = \sca{Q(}v_2\sca{)}f(v_1, v_3)$ (involved!)

### The universal property of $\GVQe$Applied to our motivating example, $\mathcal{G}(\ ) \cong \mathcal{G}^{+}(\ )$

How do we compute $\begin{CD} 1 @. @. v @. @. uv @. @. uvw @. @. \cdots @. : @. \GVQ \\ @AAA @. @AAA @. @AAA @. @AAA @. @. @. @AAFA \\ 1 @. @. v\boldsymbol{e_{-}}@. @. uv @. @. uvw\boldsymbol{e_{-}} @. @. \cdots @. : @. \mathcal{G}^{+}(V \oplus R, Q') \end{CD}$ ?

Intuition: remove $e$ from pairs that contain it

\begin{alignat*}{5} f^{-1}(e_{-}&,{}& e_{-}) &= -1 & \quad f^{-1}(v_1&,{}& v_2) &= v_1v_2 \\ f^{-1}(e_{-}&,{}& v_2) &= v_2 & \quad f^{-1}(v_1&,{}& e_{-}) &= -v_1 \end{alignat*}

By linearity, $f^{-1}(v_1+r_1e_{-}, v_2+r_2e_{-}) = (v_1 + r_1)(v_2 - r_2)$

Are we allowed to apply the universal property of $\GVQe$?

\begin{align*} f^{-1}(v{+}re_{-},v{+}re_{-}) &= v^2 - r^2 = Q'(v{+}re_{-})\,\htmlClass{c-success}{✔} \\ f^{-1}(v_1{+}r_1e,v_2{+}r_2e)f^{-1}(v_2{+}r_2e,v_3{+}r_3e_{-}) &= Q'(v_2{+}r_2e_{-})f^{-1}(v_1{+}r_1e_{-},v_3{+}r_3e_{-})\,\htmlClass{c-success}{✔}\end{align*}

#### Result

$\operatorname{of\_even} : \mathcal{G}^{+}(V\oplus R, Q') \alg{R} \GVQ \coloneqq \operatorname{lift}^{+}[f^{-1}]$

### The universal property of $\GVQe$Another example

Let's build the isomorphism $\mathcal{G}^{+}(V, Q) \cong \mathcal{G}^{+}(V, Q')$ where $Q' = -Q$.

In more concrete terms, $\mathcal{G}^{+}(\mathbb{R}^{p,q}) \cong \mathcal{G}^{+}(\mathbb{R}^{q,p})$

Note this gives $\mathbb{H} \cong \mathcal{G}(\mathbb{R}^{0,2}) \cong \mathcal{G}^{+}(\mathbb{R}^{0,3}) \emblue{\cong \mathcal{G}^{+}(\mathbb{R}^3)}$

Let $f : V \to V \to \mathcal{G}^{+}(V, Q') \coloneqq u \mapsto v \mapsto -uv$.

\begin{align*} f(v, v) &= -vv = -Q'(v) = Q(v)\,\htmlClass{c-success}{✔} \\ f(u, v)f(v, w) &= uvvw = uQ'(v)w = Q(v)(-uw)\,\htmlClass{c-success}{✔} \end{align*}

Then $\operatorname{flip\_signature} x \coloneqq \operatorname{lift}^{+}[f](x)$.

## Formalization

These algorithms did not need:

a basis on $V$,

$V$ to be finite-dimensional,

or $R$ to be a field!

Such generalization are valuable in building large libraries of formalized mathematics:

• Papers about even the most esoteric Clifford algebras can be formalized use the same definitions and terminology as more familiar GA papers.
• They flag that downstream results might also hold under unexpected generality

One such library of formalized mathematics; Lean's mathlib

### FormalizationIn the Lean theorem prover

            
variables {R V A : Type*}  -- Note: no basis, $R$ need not be a field!
variables [comm_ring R] [add_comm_group V] [module R V] [semiring A] [algebra R A]
variables (Q : quadratic_form R V)


            
/-- The universal property of $\GVQ$ -/
def lift : {f : V →ₗ[R] A // ∀ v, f v * f v = Q v • 1} ≃ (clifford_algebra Q →ₐ[R] A) :=
-- $f(v)^2 = Q(v)$


            
structure even_hom :=
(f : V →ₗ[R] V →ₗ[R] A)
(contract (v : V) : f v v = algebra_map R A (Q v))  -- $f(v, v) = Q(v)$
(contract_mid (v₁ v₂ v₃ : V) : f v₁ v₂ * f v₂ v₃ = Q v₂ • f v₁ v₃) -- $f(v_1, v_2)f(v_2, v_3) = Q(v_2)f(v_1, v_3)$

/-- The universal property of $\GVQe$ -/
def even.lift : even_hom Q A ≃ (clifford_algebra.even Q →ₐ[R] A) :=


            
/-- The isomorphism between $\GVQ$ and $\mathcal{G}^{+}(V\oplus R, Q')$ -/
def equiv_even : clifford_algebra Q ≃ₐ[R] clifford_algebra.even (Q' Q) :=



## Contributions

• Demonstrated how to view the universal property through the lens of functional programming.
• Derived a universal property for $\GVQe$ for a very general case
• Constructed the known $\GVQ \cong \mathcal{G}(V\oplus R, Q')$ using this new universal property
• Constructed the known $\GVQ \cong \bigwedge(V)$ in the same way (see paper)
• Rigorously formalized all these results in the Lean theorem prover

These slides: eric-wieser.github.io/icacga-2022
The Lean formalization: pygae.github.io/lean-ga
Everything else: efw27@cam.ac.uk

# Bonus content

Longer tutorial on the universal property: eric-wieser.github.io/brno-2021

## The isomorphism with $\bigwedge(V)$

An important result:
$\GVQ$ is isomorphic as an $R$-module to the exterior algebra $\bigwedge(V)$

\begin{align*} v\;\rfloor^f\;(uU) &= f(v, u)U - u(v\;\rfloor^f\;U)\\ \alpha^f (uU ) &= u\alpha^f (U) - u \rfloor^f (\alpha^f (U)) \end{align*}

Algèbre. Chapitre IX Bourbaki

where $f(x,y) = \pm\frac{1}{2}(Q(x+y) - Q(x) + Q(y))$

This fits into our framework!

### The isomorphism with $\bigwedge(V)$Contraction with a vector

$v\;\rfloor^f\;(uU) = f(v, u)U - u(v\;\rfloor^f\;U)$
\begin{alignat*}{7} \mkern-9mu\operatorname{ctr_{aux}}[v] : \GVQ &\to{} &\GVQ {}\mkern9mu&\mkern-9mu\oplus \GVQ& &\to{}&\GVQ {}\mkern9mu&\mkern-9mu\oplus \GVQ \\ \mkern-9mu\operatorname{ctr_{aux}}[v](u : V) &\coloneqq &(U&, x)& &\mapsto &(uU&, f(v, u)U - ux)\mkern-9mu \end{alignat*}

Verify this mets the requirements of the universal property of $\GVQ$:

\begin{align*} \operatorname{ctr_{aux}}[v](u)^2 &= (U, x) \mapsto (uuU, f(v,u)(uU) - u(f(v,u)U - ux)) \\ &= (U, x) \mapsto (Q(u)U, f(v,u)uU - f(v,u)uU + Q(u)x) \\ &= (U, x) \mapsto (Q(u)U, Q(u)x) = Q(u) \end{align*}

Evaluate at $(1, 0)$

\begin{alignat*}{4} \mkern-9mu\operatorname{ctr}[v] : \GVQ &\to{} \GVQ \\ \mkern-9mu\operatorname{ctr}[v] \coloneqq x &\mapsto c \text{ where } (x', c) = \operatorname{ctr_{aux}}[v](x, (1, 0)) \end{alignat*}

## 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$ $\Rightarrow$ $F : \mathcal{G}(V, Q) \alg{R} A$ $f : V \lin{R} A$ where $f(\vec{v})^2 = 0$ $\Rightarrow$ $F : \bigwedge(V) \alg{R} A$ $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.