Spin in dimension five as a symplectic group

For a nondegenerate quadratic form Q on a five-dimensional space over a field of characteristic not two, the even Clifford algebra C₀ is central simple of degree four (TauCeti.CliffordAlgebra.deg_even_of_finrank_eq_five), and Spin(Q) is its group U(C₀, σ) of reverse-unitary elements (CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup). The canonical involution is σ = reverse. When C₀ splits, C₀ ≃ M₄(K), this file shows that σ is symplectic: the isomorphism can be chosen to carry σ to the standard symplectic adjoint X ↦ J⁻¹ Xᵀ J = -(J Xᵀ J), and hence Spin(Q) ≅ Sp₄(K).

Without a splitting hypothesis, σ is still symplectic in the sense of involutions of central simple algebras: over any separably closed extension L / K the even Clifford algebra of the extended form splits, C₀ ⊗ L ≃ M₄(L), because it is central simple of degree four, and the split case then carries the extended reversal to the symplectic adjoint. Consequently Spin(Q) embeds in Sp₄(L), and its image is exactly the set of symplectic matrices whose preimage in C₀ ⊗ L comes from C₀: Spin(Q) is the group Sp(C₀, σ) of K-points of a twisted form of Sp₄.

The argument transports σ to an involutive anti-automorphism of M₄(K), which is the adjoint involution X ↦ C⁻¹ Xᵀ C of an invertible C with Cᵀ = ±C (Matrix.exists_forall_eq_inv_mul_transpose_mul). The sign is read off from the skew elements: the Clifford bivectors form a ten-dimensional space of even elements on which σ is -1, while an orthogonal involution of M₄(K) has at most six independent skew elements (Matrix.finrank_skewAdjointMatricesSubmodule_le_choose_two). So C is skew-symmetric, and a symplectic basis for it conjugates σ to the standard symplectic adjoint (Matrix.exists_algEquiv_inv_mul_transpose_mul_eq_neg_J_mul_transpose_mul_J).

Main definitions

• CliffordAlgebra.spinGroupEquivSymplecticGroup: an algebra isomorphism from C₀ to a matrix algebra carrying σ to the symplectic adjoint identifies Spin(Q) with the symplectic group, in dimensions one to five, via CliffordAlgebra.evenUnitaryGroupEquivSymplecticGroup.

Main results

• CliffordAlgebra.exists_algEquiv_reverseEven_eq_neg_J_mul_transpose_mul_J: in dimension five, a splitting C₀ ≃ M₄(K) can be replaced by one carrying σ to the symplectic adjoint.
• CliffordAlgebra.exists_algEquiv_reverseEven_eq_neg_J_mul_transpose_mul_J_iff: such a reversal-compatible symplectic matrix model exists exactly when C₀ splits.
• CliffordAlgebra.exists_spinGroupEquivSymplecticGroup_of_finrank_eq_five: if C₀ splits in dimension five, then Spin(Q) ≅ Sp₄(K).
• CliffordAlgebra.exists_algEquiv_reverseEven_baseChange_eq_neg_J_mul_transpose_mul_J: in dimension five, over every separably closed extension L, reversal on C₀ ⊗ L is the symplectic adjoint for a suitable splitting C₀ ⊗ L ≃ M₄(L).
• CliffordAlgebra.exists_injective_spinGroup_symplecticGroup_of_finrank_eq_five: in dimension five, Spin(Q) is the subgroup of Sp₄(L) of matrices whose preimage under such a splitting is defined over K.

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §8.D and §15.C.

noncomputable def CliffordAlgebra.spinGroupEquivSymplecticGroup {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {l : Type u_3} [Fintype l] [DecidableEq l] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 5) (e : ↥(even Q) ≃ₐ[K] Matrix (l ⊕ l) (l ⊕ l) K) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J l K * (e x).transpose * Matrix.J l K)) : ↥(spinGroup Q) ≃* ↥(Matrix.symplecticGroup l K)

In dimensions one to five, an algebra isomorphism from the even Clifford algebra to a matrix algebra of even size which carries reversal to the symplectic adjoint X ↦ -(J Xᵀ J) identifies Spin(Q) with the symplectic group. In dimension five this is Spin₅ ≅ Sp₄ for split C₀ (CliffordAlgebra.exists_spinGroupEquivSymplecticGroup_of_finrank_eq_five).

@[simp]

theorem CliffordAlgebra.coe_spinGroupEquivSymplecticGroup_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {l : Type u_3} [Fintype l] [DecidableEq l] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 5) (e : ↥(even Q) ≃ₐ[K] Matrix (l ⊕ l) (l ⊕ l) K) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J l K * (e x).transpose * Matrix.J l K)) (s : ↥(spinGroup Q)) : ↑((spinGroupEquivSymplecticGroup Q hQ hV0 hV e he) s) = e ((evenUnitaryGroupEvenPart Q) ((spinGroupToEvenUnitary Q) s))

The Spin-to-symplectic identification applies the algebra isomorphism to the underlying even Clifford element.

@[simp]

theorem CliffordAlgebra.coe_spinGroupEquivSymplecticGroup_symm_apply {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {l : Type u_3} [Fintype l] [DecidableEq l] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 5) (e : ↥(even Q) ≃ₐ[K] Matrix (l ⊕ l) (l ⊕ l) K) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J l K * (e x).transpose * Matrix.J l K)) (g : ↥(Matrix.symplecticGroup l K)) : ↑((spinGroupEquivSymplecticGroup Q hQ hV0 hV e he).symm g) = ↑(e.symm ↑g)

The inverse Spin-to-symplectic identification applies the inverse algebra isomorphism.

theorem CliffordAlgebra.exists_algEquiv_reverseEven_eq_neg_J_mul_transpose_mul_J {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hV : Module.finrank K V = 5) (e : ↥(even Q) ≃ₐ[K] Matrix (Fin 4) (Fin 4) K) : ∃ (e' : ↥(even Q) ≃ₐ[K] Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K), ∀ (x : ↥(even Q)), e' ((reverseEven Q) x) = -(Matrix.J (Fin 2) K * (e' x).transpose * Matrix.J (Fin 2) K)

Reversal is a symplectic involution in dimension five. For a quadratic form on a five-dimensional space whose even Clifford algebra splits, C₀ ≃ M₄(K), there is an algebra isomorphism C₀ ≃ M₄(K) carrying reversal to the standard symplectic adjoint X ↦ J⁻¹ Xᵀ J = -(J Xᵀ J).

theorem CliffordAlgebra.exists_algEquiv_reverseEven_eq_neg_J_mul_transpose_mul_J_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hV : Module.finrank K V = 5) : (∃ (e : ↥(even Q) ≃ₐ[K] Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) K), ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J (Fin 2) K * (e x).transpose * Matrix.J (Fin 2) K)) ↔ Nonempty (↥(even Q) ≃ₐ[K] Matrix (Fin 4) (Fin 4) K)

The dimension-five symplectic model is split exactly when the even Clifford algebra is. For a five-dimensional quadratic space, there is a matrix model carrying Clifford reversal to the standard symplectic adjoint if and only if the even Clifford algebra splits, C₀ ≃ M₄(K).

theorem CliffordAlgebra.exists_spinGroupEquivSymplecticGroup_of_finrank_eq_five {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 5) (hsplit : Nonempty (↥(even Q) ≃ₐ[K] Matrix (Fin 4) (Fin 4) K)) : Nonempty (↥(spinGroup Q) ≃* ↥(Matrix.symplecticGroup (Fin 2) K))

Split Spin₅ is Sp₄. For a nondegenerate quadratic form on a five-dimensional space whose even Clifford algebra splits, C₀ ≃ M₄(K), the group Spin(Q) is isomorphic to the symplectic group Sp₄(K).

theorem CliffordAlgebra.exists_algEquiv_reverseEven_baseChange_eq_neg_J_mul_transpose_mul_J {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (L : Type u_4) [Field L] [Algebra K L] [IsSepClosed L] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 5) : ∃ (e : ↥(even (QuadraticForm.baseChange L Q)) ≃ₐ[L] Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) L), ∀ (x : ↥(even (QuadraticForm.baseChange L Q))), e ((reverseEven (QuadraticForm.baseChange L Q)) x) = -(Matrix.J (Fin 2) L * (e x).transpose * Matrix.J (Fin 2) L)

Reversal is a symplectic involution in dimension five, with no splitting hypothesis. For a nondegenerate quadratic form on a five-dimensional space and any separably closed extension L / K, the even Clifford algebra of the extended form is isomorphic to M₄(L) by an isomorphism carrying reversal to the standard symplectic adjoint X ↦ J⁻¹ Xᵀ J = -(J Xᵀ J).

theorem CliffordAlgebra.exists_injective_spinGroup_symplecticGroup_of_finrank_eq_five {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (L : Type u_4) [Field L] [Algebra K L] [IsSepClosed L] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 5) : ∃ (e : ↥(even (QuadraticForm.baseChange L Q)) ≃ₐ[L] Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) L) (f : ↥(spinGroup Q) →* ↥(Matrix.symplecticGroup (Fin 2) L)), Function.Injective ⇑f ∧ (∀ (s : ↥(spinGroup Q)), ↑(e.symm ↑(f s)) = (ofBaseChangeAux L Q) ↑s) ∧ ∀ (g : ↥(Matrix.symplecticGroup (Fin 2) L)), g ∈ f.range ↔ ∃ y ∈ even Q, (ofBaseChangeAux L Q) y = ↑(e.symm ↑g)

Spin₅ is a twisted form of Sp₄. For a nondegenerate quadratic form on a five-dimensional space and any separably closed extension L / K, there are a splitting e : C₀ ⊗ L ≃ M₄(L) carrying reversal to the symplectic adjoint and an injective homomorphism f : Spin(Q) → Sp₄(L) with e⁻¹ (f s) the scalar extension of s. Its image consists of exactly those symplectic matrices g for which e⁻¹ g comes from C₀, so Spin(Q) is the group Sp(C₀, σ) of K-rational points of Sp₄(L) for the K-structure C₀ ⊆ C₀ ⊗ L.