Monomials of a spanning list span the Clifford algebra

Let l be a list of vectors spanning the quadratic module M. Each sublist t of l has an ordered product ι Q t₁ * ⋯ * ι Q tₖ in CliffordAlgebra Q, the monomial of t, and the monomials span the Clifford algebra as a module. Multiplying a monomial on the left by a member ι Q a of the list either adjoins a or, after moving ι Q a past the earlier factors with the Clifford relation ι Q a * ι Q b = polar Q a b - ι Q b * ι Q a, collapses ι Q a * ι Q a to the scalar Q a, so the span of the monomials is stable under left multiplication by every member of l, hence by every vector; it contains 1, hence every product of vectors, and these exhaust the Clifford algebra. No orthogonality is needed, and neither is a field or the invertibility of 2.

This is the spanning half of the Clifford analogue of the Poincaré–Birkhoff–Witt theorem. The other half, that the monomials of a basis are linearly independent, is not proved here: the low-rank identifications of the Spin group sort an element along the monomials of each length of an orthogonal basis and use only the spanning.

Main results

• CliffordAlgebra.ι_mul_mem_span_prod_map_ι_sublist: for a a member of a list l, left multiplication by ι Q a preserves the span of the monomials of l.
• CliffordAlgebra.span_prod_map_ι_sublist_eq_top: the monomials of a spanning list span the Clifford algebra.

References

• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

theorem CliffordAlgebra.ι_mul_mem_span_prod_map_ι_sublist {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} {a : M} (ha : a ∈ l) {z : CliffordAlgebra Q} (hz : z ∈ Submodule.span R ((fun (t : List M) => (List.map (⇑(ι Q)) t).prod) '' {t : List M | t.Sublist l})) : (ι Q) a * z ∈ Submodule.span R ((fun (t : List M) => (List.map (⇑(ι Q)) t).prod) '' {t : List M | t.Sublist l})

Left multiplication by a member of a list preserves the span of its monomials. Adjoining ι Q a to a monomial not containing a gives a monomial; if the monomial contains a, moving ι Q a past the earlier factors with ι Q a * ι Q b = polar Q a b - ι Q b * ι Q a and collapsing ι Q a * ι Q a to the scalar Q a gives a combination of shorter monomials.

theorem CliffordAlgebra.span_prod_map_ι_sublist_eq_top {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) : Submodule.span R ((fun (t : List M) => (List.map (⇑(ι Q)) t).prod) '' {t : List M | t.Sublist l}) = ⊤

The monomials of a spanning list span the Clifford algebra.