The Lipschitz group as the products of vectors #

Mathlib defines lipschitzGroup Q as the subgroup of (CliffordAlgebra Q)ˣ generated by the invertible vectors. This file describes that closure concretely. The inverse of a vector of invertible norm v is the vector ⅟(Q v) • v, so the generating set is closed under inversion. When 2 is invertible, the Lipschitz group is exactly the set of products of vectors of invertible norm. The scalar units are the products ι (a • v) * (ι v)⁻¹, so they lie in the Lipschitz group as soon as some vector has invertible norm.

Main results #

CliffordAlgebra.mem_lipschitzGroup_iff_exists_list: a unit lies in the Lipschitz group exactly when it is a product of vectors of invertible norm, if 2 is invertible.
CliffordAlgebra.scalarUnits: the scalar units, as a homomorphism into the Lipschitz group, whenever some vector has invertible norm.
CliffordAlgebra.scalarUnits_injective: when 2 is invertible, the scalar units embed.

References #

See C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II, and H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

The Lipschitz group as the products of vectors #

source

theorem CliffordAlgebra.mem_lipschitzGroup_of_coe_eq_prod_map_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (l : List M) (hl : ∀ v ∈ l, IsUnit (Q v)) (hx : ↑x = (List.map (⇑(ι Q)) l).prod) :

x ∈ lipschitzGroup Q

A unit that is a product of vectors of invertible norm lies in the Lipschitz group.

source

theorem CliffordAlgebra.mem_lipschitzGroup_iff_exists_list {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {x : (CliffordAlgebra Q)ˣ} :

x ∈ lipschitzGroup Q ↔ ∃ (l : List M), (∀ v ∈ l, IsUnit (Q v)) ∧ ↑x = (List.map (⇑(ι Q)) l).prod

When 2 is invertible, the Lipschitz group is the set of products of vectors of invertible norm. Mathlib defines it as the subgroup generated by the invertible vectors; since the inverse of such a vector is again a vector (coe_unitι_inv), products suffice and no inverses are needed. The converse uses Mathlib's isUnit_of_isUnit_ι to recover an invertible norm from an invertible Clifford vector; that lemma requires 2 invertible. The forward membership theorem mem_lipschitzGroup_of_coe_eq_prod_map_ι needs no hypothesis on 2.

The scalar units #

source

theorem CliffordAlgebra.unitsMap_algebraMap_mem_lipschitzGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (hQ : ∃ (v : M), IsUnit (Q v)) (a : Rˣ) :

(Units.map ↑(algebraMap R (CliffordAlgebra Q))) a ∈ lipschitzGroup Q

If some vector has invertible norm, every scalar unit lies in the Lipschitz group: it is the product ι (a • v) * (ι v)⁻¹ of two generators.

source

noncomputable def CliffordAlgebra.scalarUnits {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (hQ : ∃ (v : M), IsUnit (Q v)) :

Rˣ →* ↥(lipschitzGroup Q)

The scalar units of the Clifford algebra, as a homomorphism into the Lipschitz group. It exists as soon as some vector has invertible norm (unitsMap_algebraMap_mem_lipschitzGroup); for the zero module the Lipschitz group is trivial (lipschitzGroup_eq_bot), so no scalar unit other than 1 can lie in it.

Equations