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})$

bijective ✔, linear ✔, basis-independent ?

                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$)

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

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

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

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

              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))
            

                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)
              

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

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

Recursors

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

(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*}\]

                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]:

                  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]

                  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

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$.

RecursorsExtra inputs with the universal property

The universal property of $\GVQe$Informally

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

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

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}\]

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$

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$

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

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

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}\] ?

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

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:

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) :=
            
          

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

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

Evaluate at $(1, 0)$

Other universal properties

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

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