The Spin group in dimension at most four

For a nondegenerate quadratic space of positive dimension at most four over a field of characteristic not two, Mathlib's spinGroup fills the even unitary carrier U(C₀, σ): an even Clifford unit x with reverse x * x = 1 conjugates each vector ι v to the odd element x * ι v * reverse x, which is fixed by reversal and hence is again a vector (CliffordAlgebra.mem_range_ι_of_mem_evenOdd_one_of_reverse_eq_of_finrank_le_four); so x lies in the classical Clifford group, which is the Lipschitz group in this setting (CliffordAlgebra.mem_lipschitzGroup_of_involute_act_ι_mem_range_ι).

Dimension zero is excluded, and the exclusion is not decoration: there the Lipschitz group is trivial while the even unitary carrier is μ₂. Dimensions one and two are also covered, without nondegeneracy, by TauCeti/LinearAlgebra/CliffordAlgebra/Spin/LowRank/One.lean and TauCeti/LinearAlgebra/CliffordAlgebra/Spin/LowRank/Two.lean. The bound four is where the reversal argument stops: in dimension five the odd part also contains the volume element, which reversal fixes, and the identification needs a further argument (TauCeti/LinearAlgebra/CliffordAlgebra/Spin/LowRank/Five.lean); in dimension six the even unitary group is strictly larger than the Spin group.

Main results

• CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_le_four: for a nondegenerate form in positive dimension at most four, every even unitary Clifford unit is Lipschitz.
• CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup_of_finrank_le_four: for a nondegenerate form in positive dimension at most four, the Spin image and the even unitary carrier coincide.
• CliffordAlgebra.spinGroupEquivEvenUnitaryOfFinrankLeFour: the resulting multiplicative equivalence between the Spin group and the even unitary carrier.
• CliffordAlgebra.spinGroupEquivUnitaryOfAlgEquivOfFinrankLeFour: transport of this equivalence along any reversal-preserving algebra equivalence.

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_le_four {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 ≤ 4) : evenUnitaryGroup Q ≤ lipschitzGroup Q

For a nondegenerate quadratic space of positive dimension at most four, the even unitary carrier lies in the Lipschitz group.

theorem CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup_of_finrank_le_four {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 ≤ 4) : spinGroup.toUnits.range = evenUnitaryGroup Q

For a nondegenerate quadratic space of positive dimension at most four, the Spin group fills the even unitary carrier inside Clifford units.

noncomputable def CliffordAlgebra.spinGroupEquivEvenUnitaryOfFinrankLeFour {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 ≤ 4) : ↥(spinGroup Q) ≃* ↥(evenUnitaryGroup Q)

For a nondegenerate quadratic space of positive dimension at most four, the Spin group is multiplicatively equivalent to the even unitary carrier.

@[simp]

theorem CliffordAlgebra.spinGroupEquivEvenUnitaryOfFinrankLeFour_apply {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 ≤ 4) (s : ↥(spinGroup Q)) : (spinGroupEquivEvenUnitaryOfFinrankLeFour Q hQ hV0 hV) s = (spinGroupToEvenUnitary Q) s

The low-rank Spin/even-unitary equivalence is induced by the canonical inclusion.

noncomputable def CliffordAlgebra.spinGroupEquivUnitaryOfAlgEquivOfFinrankLeFour {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {A : Type w} [Semiring A] [Algebra K A] [StarMul A] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 4) (e : ↥(even Q) ≃ₐ[K] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) : ↥(spinGroup Q) ≃* ↥(unitary A)

A reversal-preserving algebra equivalence transports a positive, at-most-four-dimensional Spin group to the unitary group of the target algebra.

@[simp]

theorem CliffordAlgebra.coe_spinGroupEquivUnitaryOfAlgEquivOfFinrankLeFour_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {A : Type w} [Semiring A] [Algebra K A] [StarMul A] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 4) (e : ↥(even Q) ≃ₐ[K] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) (s : ↥(spinGroup Q)) : ↑((spinGroupEquivUnitaryOfAlgEquivOfFinrankLeFour Q hQ hV0 hV e he) s) = e ((evenUnitaryGroupEvenPart Q) ((spinGroupToEvenUnitary Q) s))

The transported low-rank Spin equivalence applies the target algebra equivalence to the underlying even Clifford element.

@[simp]

theorem CliffordAlgebra.coe_spinGroupEquivUnitaryOfAlgEquivOfFinrankLeFour_symm_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {A : Type w} [Semiring A] [Algebra K A] [StarMul A] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 4) (e : ↥(even Q) ≃ₐ[K] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) (q : ↥(unitary A)) : ↑((spinGroupEquivUnitaryOfAlgEquivOfFinrankLeFour Q hQ hV0 hV e he).symm q) = ↑(e.symm ↑q)

The inverse transported low-rank Spin equivalence recovers the Clifford value through the inverse target algebra equivalence.