The universal property of the even subalgebra #
Main definitions #
CliffordAlgebra.even Q: The even subalgebra of
CliffordAlgebra.EvenHom: The type of bilinear maps that satisfy the universal property of the even subalgebra
CliffordAlgebra.even.lift: The universal property of the even subalgebra, which states that every bilinear map
f v v = Q vand
f u v * f v w = Q v • f u wis in unique correspondence with an algebra morphism from
Implementation notes #
The approach here is outlined in "Computing with the universal properties of the Clifford algebra and the even subalgebra" (to appear).
The broad summary is that we have two tricks available to us for implementing complex recursors on
CliffordAlgebra.lift: the first is to use morphisms as the output type, such as
A = Module.End R N which is how we obtained
CliffordAlgebra.foldr; and the second is to use
N = (N', S) where
N' is the value we wish to compute, and
S is some auxiliary state passed
between one recursor invocation and the next.
For the universal property of the even subalgebra, we apply a variant of the first trick again by
S to itself be a submodule of morphisms.
The type of bilinear maps which are accepted by
Two algebra morphisms from the even subalgebra are equal if they agree on pairs of generators.
See note [partially-applied ext lemmas].
The final auxiliary construction for
CliffordAlgebra.even.lift. This map is the forwards
direction of that equivalence, but not in the fully-bundled form.
Every algebra morphism from the even subalgebra is in one-to-one correspondence with a bilinear map that sends duplicate arguments to the quadratic form, and contracts across multiplication.