Reversal on odd elements in dimension five

Let l be an orthogonal basis of a five-dimensional quadratic module, listed, with volume element ω = ι Q v₁ * ⋯ * ι Q v₅. The Clifford algebra is spanned by the monomials of l (TauCeti/LinearAlgebra/CliffordAlgebra/Monomials.lean), and reversal multiplies the monomial of a sublist of length k by (-1) ^ (k.choose 2): it fixes the scalars, the vectors, the products of four basis vectors and ω, and negates the products of two and of three. So for an odd element y the sum y + reverse y lies in V ⊕ R ω, and an odd element fixed by reversal lies in V ⊕ R ω as soon as 2 is invertible.

This is the dimension-five counterpart of TauCeti/LinearAlgebra/CliffordAlgebra/Reversal/Four.lean, where in dimension at most four such an element is a vector; the volume element is the one extra term, being odd and reverse-symmetric exactly when the dimension is ≡ 1 (mod 4). Its use is the identification of the Spin group in dimension five: an even unit x with reverse x * x = 1 sends a vector ι Q v to the odd element x * ι Q v * reverse x, which reversal fixes, so it is a vector plus a multiple of ω; that the multiple vanishes is a separate argument, using that ω is central.

Main results

• CliffordAlgebra.add_reverse_mem_range_ι_sup_span_of_mem_evenOdd_one_of_length_eq_five: for an orthogonal basis of length five, an odd element plus its reversal lies in V ⊕ R ω.
• CliffordAlgebra.mem_range_ι_sup_span_of_mem_evenOdd_one_of_reverse_eq_of_length_eq_five: for an orthogonal basis of length five, an odd element fixed by reversal lies in V ⊕ R ω.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

theorem CliffordAlgebra.add_reverse_mem_range_ι_sup_span_of_mem_evenOdd_one_of_length_eq_five {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) (hlen : l.length = 5) {y : CliffordAlgebra Q} (hy : y ∈ evenOdd Q 1) : y + reverse y ∈ (ι Q).range ⊔ R ∙ (List.map (⇑(ι Q)) l).prod

For an orthogonal basis of length five, an odd element plus its reversal is a vector plus a multiple of the volume element. Reversal multiplies the monomial of k basis vectors by (-1) ^ (k.choose 2), which is 1 for k = 0, 1, 4, 5 and -1 for k = 2, 3; the monomials of length 0 and 4 are even and drop out of an odd element.

theorem CliffordAlgebra.mem_range_ι_sup_span_of_mem_evenOdd_one_of_reverse_eq_of_length_eq_five {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) (hlen : l.length = 5) {y : CliffordAlgebra Q} (hy : y ∈ evenOdd Q 1) (hrev : reverse y = y) : y ∈ (ι Q).range ⊔ R ∙ (List.map (⇑(ι Q)) l).prod

For an orthogonal basis of length five, an odd element fixed by reversal is a vector plus a multiple of the volume element.