The norm of the Lipschitz group

The Clifford norm star x * x of a Lipschitz element is a unit scalar. This defines a homomorphism from the Lipschitz group to the units of the base ring. Generating vectors have norm the negative of their quadratic norm.

Together with the orthogonal action, this homomorphism is the input for the general-field spinor norm: the Clifford norm descends modulo squares through the kernel of that action.

Main results

• CliffordAlgebra.lipschitzNorm: the unit-valued Clifford norm.
• CliffordAlgebra.self_mul_star_eq_algebraMap_lipschitzNorm: its second characteristic Clifford-product equation.
• CliffordAlgebra.lipschitzNorm_unitι: its value on a generating vector.
• CliffordAlgebra.mem_pinGroup_iff_lipschitzNorm_eq_one: the Pin group is cut out of the Lipschitz group by this norm.
• CliffordAlgebra.lipschitzNorm_scalarUnits: the norm of a scalar unit is its square.

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

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

The unit-valued Clifford norm on the Lipschitz group.

Equations

• CliffordAlgebra.lipschitzNorm Q = { toFun := CliffordAlgebra.lipschitzNormUnit✝ Q, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CliffordAlgebra.star_mul_self_eq_algebraMap_lipschitzNorm {R : Type u} {V : Type v} [CommRing R] [AddCommGroup V] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : ↥(lipschitzGroup Q)) : star ↑↑x * ↑↑x = (algebraMap R (CliffordAlgebra Q)) ↑((lipschitzNorm Q) x)

The product of the Clifford conjugate of a Lipschitz element with itself is its scalar norm.

@[simp]

theorem CliffordAlgebra.self_mul_star_eq_algebraMap_lipschitzNorm {R : Type u} {V : Type v} [CommRing R] [AddCommGroup V] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : ↥(lipschitzGroup Q)) : ↑↑x * star ↑↑x = (algebraMap R (CliffordAlgebra Q)) ↑((lipschitzNorm Q) x)

The product of a Lipschitz element with its Clifford conjugate is its scalar norm.

@[simp]

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

A generating vector has Clifford norm equal to the negative of its quadratic norm.

@[simp]

theorem CliffordAlgebra.mem_pinGroup_iff_lipschitzNorm_eq_one {R : Type u} {V : Type v} [CommRing R] [AddCommGroup V] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : ↥(lipschitzGroup Q)) : ↑↑x ∈ pinGroup Q ↔ (lipschitzNorm Q) x = 1

A Lipschitz element lies in the Pin group exactly when its lipschitzNorm is one.

theorem CliffordAlgebra.lipschitzNorm_eq_of_coe_eq_algebraMap {R : Type u} {V : Type v} [CommRing R] [AddCommGroup V] [Module R V] [Invertible 2] {Q : QuadraticForm R V} {x : ↥(lipschitzGroup Q)} {a : Rˣ} (hx : ↑↑x = (algebraMap R (CliffordAlgebra Q)) ↑a) : (lipschitzNorm Q) x = a * a

A Lipschitz element equal to a scalar unit has norm equal to the square of that scalar.

@[simp]

theorem CliffordAlgebra.lipschitzNorm_scalarUnits {R : Type u} {V : Type v} [CommRing R] [AddCommGroup V] [Module R V] [Invertible 2] {Q : QuadraticForm R V} (hQ : ∃ (v : V), IsUnit (Q v)) (a : Rˣ) : (lipschitzNorm Q) ((scalarUnits Q hQ) a) = a * a

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