The Spin group in dimensions one to five

For a nondegenerate quadratic space of dimension between one and five over a field of characteristic not two, Mathlib's spinGroup fills the even unitary carrier U(C₀, σ). Dimensions at most four are TauCeti/LinearAlgebra/CliffordAlgebra/Spin/LowRank/Four.lean; this file adds dimension five and assembles the range.

In dimension five an even unitary unit x still conjugates each vector ι Q v to an odd, reverse-fixed element y = x * ι Q v * x⁻¹, but now such an element is a vector plus a multiple of the volume element ω of an orthogonal basis (CliffordAlgebra.mem_range_ι_sup_span_of_mem_evenOdd_one_of_reverse_eq_of_length_eq_five), y = ι Q w + c • ω. The square of y is the scalar Q v, and ω is central with scalar square, so the cross term 2 c • (ω * ι Q w) is a scalar: either c = 0, or ι Q w is a multiple of the central ω, hence central, hence zero, in which case y = c • ω is itself central and equals ι Q v. Either way y is a vector, so x lies in the classical Clifford group, which is the Lipschitz group (CliffordAlgebra.mem_lipschitzGroup_of_involute_act_ι_mem_range_ι).

Dimension five is where the identification stops: in dimension six the even unitary group is strictly larger than the Spin group (TauCeti/LinearAlgebra/CliffordAlgebra/Spin/LowRank/Six/Basic.lean), the volume element being then reverse-antisymmetric and anticommuting with the vectors.

Main results

• CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_five: for a nondegenerate form in dimension five, every even unitary Clifford unit is Lipschitz.
• CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup: for a nondegenerate form in dimension between one and five, every even unitary Clifford unit is Lipschitz.
• CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup: for a nondegenerate form in dimension between one and five, the Spin image and the even unitary carrier coincide.

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §15.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

theorem CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_five {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 5) : evenUnitaryGroup Q ≤ lipschitzGroup Q

In dimension five, the even unitary carrier lies in the Lipschitz group.

theorem CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 5) : evenUnitaryGroup Q ≤ lipschitzGroup Q

Spin is the even unitary group in dimensions one to five. For a nondegenerate quadratic space of dimension between one and five, the even unitary carrier lies in the Lipschitz group. Dimension zero is excluded, and the exclusion is not decoration: there the Lipschitz group is trivial while the even unitary carrier is μ₂. The bound five is sharp, by CliffordAlgebra.not_evenUnitaryGroup_le_lipschitzGroup_of_six_le_finrank.

theorem CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 5) : spinGroup.toUnits.range = evenUnitaryGroup Q

For a nondegenerate quadratic space of dimension between one and five, the Spin group fills the even unitary carrier inside Clifford units.