The kernel of the Lipschitz action

The Lipschitz group acts on its quadratic space by twisted conjugation, lipschitzToOrthogonal Q : lipschitzGroup Q →* O(Q). Scalars act trivially. Conversely, an element acting trivially graded-commutes with every vector, and for a nondegenerate form on a finite-dimensional space over a field in which 2 is invertible such an element is a scalar (CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul). When a vector has invertible norm, the scalar units lie in the Lipschitz group and form exactly the kernel of the action. This is the statement that makes the spinor norm of an isometry independent of the Lipschitz element chosen to lift it: two lifts differ by a scalar.

Main results

• CliffordAlgebra.lipschitzToOrthogonal_eq_one_of_coe_eq_algebraMap: a scalar acts trivially.
• CliffordAlgebra.mem_ker_lipschitzToOrthogonal_iff: an element of the Lipschitz group acts trivially exactly when it is a scalar unit.
• CliffordAlgebra.ker_lipschitzToOrthogonal: when a vector has invertible norm, the kernel of the Lipschitz action is the range of CliffordAlgebra.scalarUnits.

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.

theorem CliffordAlgebra.lipschitzToOrthogonal_eq_one_of_coe_eq_algebraMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {x : ↥(lipschitzGroup Q)} {a : R} (hx : ↑↑x = (algebraMap R (CliffordAlgebra Q)) a) : (lipschitzToOrthogonal Q) x = 1

A Lipschitz element that is a scalar acts trivially on the quadratic space.

@[simp]

theorem CliffordAlgebra.lipschitzToOrthogonal_scalarUnits {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (hQ : ∃ (v : M), IsUnit (Q v)) (a : Rˣ) : (lipschitzToOrthogonal Q) ((scalarUnits Q hQ) a) = 1

The scalar units act trivially on the quadratic space.

theorem CliffordAlgebra.mem_ker_lipschitzToOrthogonal_iff {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) {x : ↥(lipschitzGroup Q)} : x ∈ (lipschitzToOrthogonal Q).ker ↔ ∃ (r : Kˣ), ↑↑x = (algebraMap K (CliffordAlgebra Q)) ↑r

An element of the Lipschitz group acts trivially exactly when it is a scalar unit, for a nondegenerate form on a finite-dimensional space over a field in which 2 is invertible.

theorem CliffordAlgebra.ker_lipschitzToOrthogonal {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)) : (lipschitzToOrthogonal Q).ker = (scalarUnits Q hv).range

The kernel of the Lipschitz action is the group of scalar units, for a nondegenerate form on a finite-dimensional space over a field in which 2 is invertible, provided some vector is anisotropic so that the scalar units lie in the Lipschitz group.