The Spin group is strictly smaller than the even unitary group in dimension six

For a nondegenerate quadratic form in dimensions one to five, the Spin group is the whole even unitary group U(C₀, σ) of the Clifford algebra: every even Clifford unit x with reverse x * x = 1 lies in the Lipschitz group. The sibling files prove this in dimensions one and two. This file shows that the equality stops in dimension six, where U(C₀, σ) is a unitary group of degree four and the Spin group is only its reduced-norm-one subgroup, and that, for nondegenerate forms over infinite fields in which 2 ≠ 0, it fails in every dimension from six on.

The witness is explicit. Let v₁, …, vₙ be pairwise orthogonal anisotropic vectors, where n is even and n.choose 2 is odd (that is, n ≡ 2 (mod 4)), and let ω = ι v₁ ⋯ ι vₙ be their volume element. It is even, it anticommutes with each of the ι vᵢ, its reverse is -ω, and its square is the scalar -(Q v₁ ⋯ Q vₙ). Hence x = a + b • ω is an even unit with reverse x * x = a² + b² ∏ Q vᵢ, so x ∈ U(C₀, σ) as soon as a² + b² ∏ Q vᵢ = 1. Twisted conjugation by x sends each of the listed vectors v to (a² - b² ∏ Q vᵢ) • v + 2ab • ω v, and once n ≥ 3 the element ω v is not a vector: any anisotropic u ⟂ v among the list would commute with it, forcing it to be proportional to u, and two orthogonal choices of u leave only 0. Since the Lipschitz group preserves the vectors under twisted conjugation, x is not in it whenever a b ≠ 0. Over an infinite field in which 2 ≠ 0 the conic a² + δ b² = 1 always has such a point. The smallest admissible length is n = 6, which is the dimension-six application.

The witness only uses the listed orthogonal anisotropic vectors, not a basis, so it lives in the Clifford algebra of every nondegenerate form of dimension at least six, and the theorems about it carry no hypothesis on the ambient dimension. (In a larger space ω commutes with a further orthogonal vector rather than anticommuting with it; only the listed vectors are used.) The same computation is why dimension two is different: n = 2 also has n ≡ 2 (mod 4), but there ω v is a multiple of the other basis vector, and indeed the Spin group fills the even unitary group in dimension two.

The dimension-six identification Spin(Q) ≅ SU(C₀, σ) and the strictness SU ≠ U are classical; see M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §15, and H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

Main results

• CliffordAlgebra.exists_mem_evenUnitaryGroup_coe_eq_algebraMap_add_smul_prod_map_ι: for ω the volume element of an orthogonal list of even length with odd n.choose 2, in any quadratic module over a commutative ring containing it, a + b • ω is an even unitary unit when a² + b² ∏ Q vᵢ = 1.
• CliffordAlgebra.notMem_lipschitzGroup_of_mem_evenUnitaryGroup_of_coe_eq: such a unit with a b ≠ 0 is not in the Lipschitz group once the list is anisotropic of length at least three.
• CliffordAlgebra.range_spinGroup_toUnits_ne_evenUnitaryGroup_of_six_le_finrank: over an infinite field in which 2 ≠ 0, the Spin group of a nondegenerate form of dimension at least six is a proper subgroup of the even unitary group.
• CliffordAlgebra.exists_spinGroup_ne_evenUnitaryGroup_finrank_six: the split rational witness, a nondegenerate form on Fin 6 → ℚ whose Spin group is a proper subgroup of its even unitary group.

The conic point is TauCeti.exists_sq_add_sq_mul_eq_one (TauCeti/Algebra/Field/Conic.lean), and the fact that ω v is not a vector is CliffordAlgebra.prod_map_ι_mul_ι_notMem_range_ι (TauCeti/LinearAlgebra/CliffordAlgebra/VolumeElement.lean).

Auxiliary volume-element computations

The witness a + b • ω built from an orthogonal list of length ≡ 2 (mod 4)

theorem CliffordAlgebra.exists_mem_evenUnitaryGroup_coe_eq_algebraMap_add_smul_prod_map_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (heven : Even l.length) (hodd : Odd (l.length.choose 2)) {a b : R} (hab : a ^ 2 + b ^ 2 * (List.map (⇑Q) l).prod = 1) : ∃ x ∈ evenUnitaryGroup Q, ↑x = (algebraMap R (CliffordAlgebra Q)) a + b • (List.map (⇑(ι Q)) l).prod

The even unitary units a + b • ω built from an orthogonal list of even length with odd n.choose 2. For ω the volume element of such a list (its length is ≡ 2 (mod 4)), in any quadratic module over a commutative ring containing the list, a + b • ω is an even unitary unit as soon as a² + b² ∏ Q vᵢ = 1. Neither anisotropy nor a field is needed at this stage; both enter only when the unit is shown to lie outside the Lipschitz group.

The witness is not in the Lipschitz group

theorem CliffordAlgebra.notMem_lipschitzGroup_of_mem_evenUnitaryGroup_of_coe_eq {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {l : List V} [Invertible 2] (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (heven : Even l.length) (hodd : Odd (l.length.choose 2)) (h3 : 3 ≤ l.length) (haniso : ∀ v ∈ l, Q v ≠ 0) {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ evenUnitaryGroup Q) {a b : K} (hcoe : ↑x = (algebraMap K (CliffordAlgebra Q)) a + b • (List.map (⇑(ι Q)) l).prod) (ha : a ≠ 0) (hb : b ≠ 0) : x ∉ lipschitzGroup Q

An even unitary unit a + b • ω with a b ≠ 0 is not in the Lipschitz group, for ω the volume element of an orthogonal anisotropic list of even length at least three with odd n.choose 2. Length two is genuinely excluded: there ω sends each member of the list to a multiple of the other. The list need not span: the witness lives in the Clifford algebra of any quadratic space containing it.

theorem CliffordAlgebra.not_evenUnitaryGroup_le_lipschitzGroup_of_sq_add_sq_mul_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {l : List V} [Invertible 2] (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (heven : Even l.length) (hodd : Odd (l.length.choose 2)) (h3 : 3 ≤ l.length) (haniso : ∀ v ∈ l, Q v ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ^ 2 + b ^ 2 * (List.map (⇑Q) l).prod = 1) : ¬evenUnitaryGroup Q ≤ lipschitzGroup Q

Given an orthogonal anisotropic list of even length at least three with odd n.choose 2, the even unitary group is not contained in the Lipschitz group as soon as a² + b² ∏ Q vᵢ = 1 has a solution with a b ≠ 0, the witness being a + b • ω for ω the volume element of the list.

Infinite fields with 2 ≠ 0: every nondegenerate form of dimension at least six

theorem CliffordAlgebra.not_evenUnitaryGroup_le_lipschitzGroup_of_six_le_finrank {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Infinite K] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : 6 ≤ Module.finrank K V) : ¬evenUnitaryGroup Q ≤ lipschitzGroup Q

Over an infinite field in which 2 ≠ 0, the even unitary group of a nondegenerate quadratic form of dimension at least six is not contained in the Lipschitz group. The witness is a + b • ω for ω the volume element of six members of an orthogonal basis, six being the smallest length ≡ 2 (mod 4) that is at least three.

theorem CliffordAlgebra.range_spinGroup_toUnits_ne_evenUnitaryGroup_of_six_le_finrank {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Infinite K] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : 6 ≤ Module.finrank K V) : spinGroup.toUnits.range ≠ evenUnitaryGroup Q

Over an infinite field in which 2 ≠ 0, the Spin group of a nondegenerate quadratic form of dimension at least six is a proper subgroup of the even unitary group inside Clifford units. This is where the low-rank identification of Spin with the even unitary group stops.

The split rational witness

theorem CliffordAlgebra.exists_spinGroup_ne_evenUnitaryGroup_finrank_six : ∃ (Q : QuadraticForm ℚ (Fin 6 → ℚ)), QuadraticMap.Nondegenerate ∧ spinGroup.toUnits.range ≠ evenUnitaryGroup Q

A split rational witness: the diagonal form ⟨1, -1, 1, -1, 1, -1⟩ on Fin 6 → ℚ, the diagonalisation of the split form H ⟂ H ⟂ H, is a nondegenerate form of dimension six whose Spin group is a proper subgroup of its even unitary group. This is the classical example where U(C₀, σ) ≅ GL₄(ℚ) and Spin(Q) ≅ SL₄(ℚ).