The Lipschitz group as the twisted-conjugation stabiliser of the vectors

Mathlib defines lipschitzGroup Q as the subgroup of Clifford units generated by the invertible vectors and proves that twisted conjugation v ↦ involute x * ι Q v * x⁻¹ by such a unit carries vectors to vectors (lipschitzGroup.involute_act_ι_mem_range_ι), recording as an open question whether, in finite dimensions, every unit whose twisted conjugation preserves the vectors — an element of the classical Clifford group — is generated by invertible vectors. This file settles that question for a nondegenerate form representing a unit on a finite-dimensional space over a field of characteristic not two, where the two groups coincide. For a nondegenerate form, representing a unit is the same as having positive dimension, and the hypothesis cannot be dropped: on the zero space the Lipschitz group is trivial, while every scalar unit preserves the zero space of vectors.

Twisted conjugation by such a unit x induces the linear endomorphism CliffordAlgebra.vectorMap of the quadratic space; it preserves the form (CliffordAlgebra.vectorMap_map_app_of_involute_act_ι_mem_range_ι) and is injective because x is a unit, hence is an isometry. By Cartan–Dieudonné some Lipschitz element y induces the same isometry (CliffordAlgebra.lipschitzToOrthogonal_surjective), so y⁻¹ * x graded-commutes with every vector and is a scalar (CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul). Scalar units lie in the Lipschitz group as soon as some vector is anisotropic.

Main results

• CliffordAlgebra.mem_lipschitzGroup_of_involute_act_ι_mem_range_ι: for a nondegenerate form representing a unit, a unit whose twisted conjugation preserves the vectors lies in the Lipschitz group.
• CliffordAlgebra.mem_lipschitzGroup_iff_involute_act_ι_mem_range_ι: for a nondegenerate form representing a unit, the Lipschitz group is exactly the classical Clifford group.
• CliffordAlgebra.mem_spinGroup_iff_unitary_even_and_involute_act_ι_mem_range_ι: under the same hypotheses, Mathlib's Spin group consists of the even unitary elements whose twisted conjugation preserves the vectors, with no reference to the Lipschitz closure.

References

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

theorem CliffordAlgebra.mem_lipschitzGroup_of_involute_act_ι_mem_range_ι {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hv : ∃ (v : V), IsUnit (Q v)) {x : (CliffordAlgebra Q)ˣ} (hx : ∀ (m : V), involute ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range) : x ∈ lipschitzGroup Q

A unit whose twisted conjugation preserves the vectors is a Lipschitz element. For a nondegenerate form on a finite-dimensional space representing a unit, Mathlib's closure-defined Lipschitz group contains the classical Clifford group.

theorem CliffordAlgebra.mem_lipschitzGroup_iff_involute_act_ι_mem_range_ι {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hv : ∃ (v : V), IsUnit (Q v)) {x : (CliffordAlgebra Q)ˣ} : x ∈ lipschitzGroup Q ↔ ∀ (m : V), involute ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range

Mathlib's Lipschitz group is the classical Clifford group. For a nondegenerate form on a finite-dimensional space representing a unit, a Clifford unit is generated by invertible vectors exactly when its twisted conjugation preserves the vectors.

theorem CliffordAlgebra.mem_spinGroup_iff_unitary_even_and_involute_act_ι_mem_range_ι {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hv : ∃ (v : V), IsUnit (Q v)) {x : CliffordAlgebra Q} : x ∈ spinGroup Q ↔ x ∈ unitary (CliffordAlgebra Q) ∧ x ∈ even Q ∧ ∀ (m : V), involute x * (ι Q) m * star x ∈ (ι Q).range

Mathlib's Spin group is the even unitary Clifford group. For a nondegenerate form on a finite-dimensional space representing a unit, an element of the Clifford algebra lies in spinGroup Q exactly when it is unitary, even, and its twisted conjugation v ↦ involute x * ι Q v * star x preserves the vectors. Unitarity makes star x the inverse of x, so this is the Lipschitz condition of mem_lipschitzGroup_iff_involute_act_ι_mem_range_ι read on the Clifford algebra itself.