Even Clifford elements in dimension one

Every even element of a rank-one Clifford algebra is the image of a scalar, over any field, including one of characteristic two. The corresponding statement for units follows from the unit-lifting lemma for a homomorphism out of a group with zero.

The scalar calculation follows the standard Clifford algebra argument; see H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

Main results

• CliffordAlgebra.exists_eq_algebraMap_of_mem_even_of_finrank_eq_one: every even element is a scalar in dimension one.
• CliffordAlgebra.exists_eq_unitsMap_algebraMap_of_mem_even_of_finrank_eq_one: every even unit comes from a unit of the base field.

theorem CliffordAlgebra.exists_eq_algebraMap_of_mem_even_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hV : Module.finrank K V = 1) (y : CliffordAlgebra Q) (hy : y ∈ even Q) : ∃ (a : K), y = (algebraMap K (CliffordAlgebra Q)) a

In dimension one, every even Clifford element equals the image of a scalar, over any field.

theorem CliffordAlgebra.exists_eq_unitsMap_algebraMap_of_mem_even_of_finrank_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hV : Module.finrank K V = 1) (x : (CliffordAlgebra Q)ˣ) (hx : ↑x ∈ even Q) : ∃ (a : Kˣ), x = (Units.map ↑(algebraMap K (CliffordAlgebra Q))) a

In dimension one, every even Clifford unit equals the image of a unit of the base field.