The reverse norm of the Lipschitz group

A Clifford algebra carries two anti-involutions that fix the scalars: the reversion reverse, which fixes every vector, and Mathlib's star = reverse ∘ involute, which negates every vector. Each gives a norm on the Lipschitz group. The star norm lipschitzNorm takes the value -Q v on a vector v. This file develops the reverse norm x ↦ reverse x * x, which takes the value Q v on the nose, so a spinor norm defined through it sends the reflection in v to the square class of Q v rather than of -Q v.

The two norms agree on even elements and differ by the sign (-1) ^ r on a product of r vectors. Since the square class of -1 is in general nontrivial, they genuinely differ on odd Lipschitz elements. Mathlib's Pin and Spin groups are cut out by the star norm. On the even part the two norms agree, so the Spin group is exactly the set of even Lipschitz elements of reverse norm one.

Main results

• CliffordAlgebra.reverse_prod_map_ι_mul_prod_map_ι: the reverse norm of a product of vectors is the product of their quadratic norms.
• CliffordAlgebra.star_mul_self_eq_reverse_mul_self_of_mem_even and CliffordAlgebra.star_mul_self_eq_neg_one_pow_smul_reverse_mul_self: the two norms agree on even elements and differ by (-1) ^ r on a product of r vectors.
• CliffordAlgebra.cliffordNorm: the unit-valued reverse norm on the Lipschitz group, with its defining equation CliffordAlgebra.reverse_mul_self_eq_algebraMap_cliffordNorm.
• CliffordAlgebra.cliffordNorm_comp_lipschitzGroupMap and CliffordAlgebra.cliffordNorm_comp_lipschitzGroupBaseChange: the Clifford norm is natural under quadratic isometries and extension of scalars.
• CliffordAlgebra.cliffordNorm_unitι: a vector v with unit Q v has reverse norm Q v.
• CliffordAlgebra.cliffordNorm_eq_sq_mul_of_coe_eq_algebraMap_mul: rescaling by a scalar unit c multiplies the reverse norm by c ^ 2.
• CliffordAlgebra.cliffordNorm_scalarUnits: a scalar unit has reverse norm equal to its square.
• CliffordAlgebra.lipschitzNorm_eq_cliffordNorm_of_mem_even and CliffordAlgebra.lipschitzNorm_eq_neg_cliffordNorm_of_mem_odd: the comparison with the star norm on the Lipschitz group.
• CliffordAlgebra.mem_spinGroup_iff_mem_even_and_cliffordNorm_eq_one: the Spin group consists of the even Lipschitz elements of reverse norm one.
• CliffordAlgebra.exists_scalarUnits_mul_mem_spinGroup_iff: a Lipschitz element rescales by a scalar unit into the Spin group exactly when it is even and its reverse norm is a square.

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2, and T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter V §3.

The reverse norm on the Lipschitz group

noncomputable def CliffordAlgebra.cliffordNorm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(lipschitzGroup Q) →* Rˣ

The Clifford norm x ↦ reverse x * x on the Lipschitz group, as a unit-valued homomorphism. It takes the value Q v when Q v is a unit (cliffordNorm_unitι). It agrees with the star norm lipschitzNorm on even elements and is its negative on odd ones.

Equations

• CliffordAlgebra.cliffordNorm Q = { toFun := CliffordAlgebra.cliffordNormUnit✝ Q, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CliffordAlgebra.reverse_mul_self_eq_algebraMap_cliffordNorm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) : reverse ↑↑x * ↑↑x = (algebraMap R (CliffordAlgebra Q)) ↑((cliffordNorm Q) x)

The defining equation of the Clifford norm: reverse x * x is the scalar cliffordNorm Q x.

@[simp]

theorem CliffordAlgebra.self_mul_reverse_eq_algebraMap_cliffordNorm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) : ↑↑x * reverse ↑↑x = (algebraMap R (CliffordAlgebra Q)) ↑((cliffordNorm Q) x)

The Clifford norm is also the scalar x * reverse x.

Naturality

@[simp]

theorem CliffordAlgebra.cliffordNorm_lipschitzGroupMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {N : Type u_1} [AddCommGroup N] [Module R N] {Q' : QuadraticForm R N} (f : Q →qᵢ Q') (x : ↥(lipschitzGroup Q)) : (cliffordNorm Q') (f.lipschitzGroupMap x) = (cliffordNorm Q) x

The Clifford norm is unchanged when a Lipschitz element is mapped along a quadratic isometry.

@[simp]

theorem CliffordAlgebra.cliffordNorm_comp_lipschitzGroupMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {N : Type u_1} [AddCommGroup N] [Module R N] {Q' : QuadraticForm R N} (f : Q →qᵢ Q') : (cliffordNorm Q').comp f.lipschitzGroupMap = cliffordNorm Q

The Clifford norm commutes with the map of Lipschitz groups induced by a quadratic isometry.

@[simp]

theorem CliffordAlgebra.cliffordNorm_lipschitzGroupBaseChange {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {A : Type u_1} [CommRing A] [Algebra R A] (x : ↥(lipschitzGroup Q)) : (cliffordNorm (QuadraticForm.baseChange A Q)) ((lipschitzGroupBaseChange Q) x) = (Units.map ↑(algebraMap R A)) ((cliffordNorm Q) x)

Extending a Lipschitz element's scalars sends its Clifford norm along the induced map on units.

@[simp]

theorem CliffordAlgebra.cliffordNorm_comp_lipschitzGroupBaseChange {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {A : Type u_1} [CommRing A] [Algebra R A] : (cliffordNorm (QuadraticForm.baseChange A Q)).comp (lipschitzGroupBaseChange Q) = (Units.map ↑(algebraMap R A)).comp (cliffordNorm Q)

The Clifford norm commutes with extension of scalars on the Lipschitz group.

@[simp]

theorem CliffordAlgebra.cliffordNorm_unitι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (v : M) [Invertible (Q v)] : (cliffordNorm Q) ⟨unitι Q v, ⋯⟩ = unitOfInvertible (Q v)

A vector v with unit Q v has Clifford norm Q v, with no sign.

theorem CliffordAlgebra.cliffordNorm_eq_sq_mul_of_coe_eq_algebraMap_mul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {x y : ↥(lipschitzGroup Q)} {c : Rˣ} (h : ↑↑y = (algebraMap R (CliffordAlgebra Q)) ↑c * ↑↑x) : (cliffordNorm Q) y = c ^ 2 * (cliffordNorm Q) x

Rescaling a Lipschitz element by a scalar unit c multiplies its Clifford norm by c ^ 2.

@[simp]

theorem CliffordAlgebra.cliffordNorm_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)) (c : Rˣ) : (cliffordNorm Q) ((scalarUnits Q hQ) c) = c * c

The Clifford norm of a scalar unit in the Lipschitz group is its square.

Comparison with the star norm and the Spin group

theorem CliffordAlgebra.lipschitzNorm_eq_cliffordNorm_of_mem_even {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) (hx : ↑↑x ∈ evenOdd Q 0) : (lipschitzNorm Q) x = (cliffordNorm Q) x

On an even Lipschitz element, the star norm equals the Clifford norm.

theorem CliffordAlgebra.lipschitzNorm_eq_neg_cliffordNorm_of_mem_odd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) (hx : ↑↑x ∈ evenOdd Q 1) : (lipschitzNorm Q) x = -(cliffordNorm Q) x

On an odd Lipschitz element, the star norm is the negative of the Clifford norm.

@[simp]

theorem CliffordAlgebra.mem_spinGroup_iff_mem_even_and_cliffordNorm_eq_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) : ↑↑x ∈ spinGroup Q ↔ ↑↑x ∈ evenOdd Q 0 ∧ (cliffordNorm Q) x = 1

Mathlib's Spin group, read through the Clifford norm. A Lipschitz element lies in spinGroup Q exactly when it is even and its Clifford norm reverse x * x is one.

@[simp]

theorem CliffordAlgebra.cliffordNorm_pinToLipschitz_spinToPin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(spinGroup Q)) : (cliffordNorm Q) ((pinToLipschitz Q) ((spinToPin Q) x)) = 1

A Spin element has Clifford norm one.

theorem CliffordAlgebra.exists_scalarUnits_mul_mem_spinGroup_iff {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)) (x : ↥(lipschitzGroup Q)) : (∃ (a : Rˣ), ↑↑((scalarUnits Q hQ) a * x) ∈ spinGroup Q) ↔ ↑↑x ∈ evenOdd Q 0 ∧ IsSquare ((cliffordNorm Q) x)

Rescaling a Lipschitz element into the Spin group. A Lipschitz element can be multiplied by a scalar unit into spinGroup Q exactly when it is even and its Clifford norm is a square. Rescaling by a multiplies the Clifford norm by a * a and preserves evenness.