Spin groups of polarized six-dimensional quadratic spaces

Let (V, Q) be a six-dimensional quadratic space with a polarization V = W ⊕ W' into two isotropic subspaces of dimension three, over a field of characteristic not two. The even Clifford algebra acts on the even half S⁺ = ⋀ᵉᵛᵉⁿ W of the Fock module, a space of dimension four. This file proves that this half-spin action identifies Spin(Q) with the special linear group of S⁺:

• every Spin element acts on S⁺ with determinant one;
• every endomorphism of S⁺ of determinant one is the action of a Spin element.

In the matrix-product model of the even Clifford algebra of three hyperbolic planes, TauCeti.hyperbolicSixEvenUnitaryEquivGeneralLinear identifies the reverse-unitary group U(C₀, σ) with GL₄(K). Under that identification Spin(Q) is exactly the determinant-one subgroup, so Spin(Q) ≅ SL₄(K). Over ℚ this is the split rational witness that the inclusion Spin(Q) ≤ U(C₀, σ) is strict in dimension six, with U(C₀, σ) ≅ GL₄(ℚ) and Spin(Q) ≅ SL₄(ℚ).

The argument

Write e₀, e₁, e₂ for a basis of W. The even half S⁺ has basis 1, e₀e₁, e₀e₂, e₁e₂. A vector v = w + w' acts on the Fock module ⋀W by s ↦ w ∧ s + ⌊w'⌋ s. Fix v₀ = e₀ + f₀, where f₀ is the vector of W' dual to e₀, so that Q v₀ = 1. The actions of ι v₀ * ι v and of ι v * ι v₀ on S⁺ are explicit four-by-four matrices whose entries are the coordinates of v, and each has determinant (Q v) ^ 2. Since ι v₀ * ι v₀ = 1, the action of ι u * ι v therefore has determinant (Q u) ^ 2 * (Q v) ^ 2. Mathlib's Lipschitz group consists of products of vectors (CliffordAlgebra.mem_lipschitzGroup_iff_exists_list), so a Spin element acts on S⁺ with determinant the square of its reverse norm, which is one.

Conversely, the canonical Spin lifts 1 + ι w * ι u of the Eichler transvections, for u and w among the basis vectors of W and W', act on S⁺ as the twelve elementary transvections in the basis above. These generate the special linear group.

Main results

• TauCeti.det_spinPlusAction_spinGroupToEven: a Spin element of a polarized six-dimensional space acts on the even half-spin module with determinant one.
• TauCeti.exists_spinPlusAction_spinGroupToEven_eq_of_det_eq_one: every determinant-one endomorphism of the even half-spin module is the action of a Spin element.
• TauCeti.spinSixTransvectionLift: a specified Spin lift of each elementary transvection, with its half-spin matrix and vector action computed explicitly.
• TauCeti.mem_range_spinGroupToEvenUnitary_iff_det_hyperbolicSixEvenUnitaryEquivGeneralLinear: for three hyperbolic planes, an even unitary element lies in Spin exactly when its image in GL₄(K) has determinant one.
• TauCeti.hyperbolicSixSpinEquivSpecialLinear: the Spin group of three hyperbolic planes is SL₄(K), compatibly with TauCeti.hyperbolicSixEvenUnitaryEquivGeneralLinear; it specializes the polarized construction below.
• TauCeti.spinGroupEquivSpecialLinearGroupOfFinrankEqSix: the Spin-to-SL₄ equivalence for a polarized six-dimensional quadratic space.
• TauCeti.coe_spinGroupEquivSpecialLinearGroupOfFinrankEqSix_apply: its matrix formula in the basis TauCeti.spinPlusFinBasisOfFinrankEqSix used by Algebra.endAlgEquivMatrix.

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §15.D.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 20.
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

Coordinate data

noncomputable def Module.Basis.spinSixEvenMonomial {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (b : Basis (Fin 3) R M) : Fin 4 → _root_.ExteriorAlgebra R M

The ordered even monomials 1, e₀e₁, e₀e₂, e₁e₂.

@[simp]

theorem Module.Basis.spinSixEvenMonomial_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (b : Basis (Fin 3) R M) (j : Fin 4) : b.spinSixEvenMonomial j = ![1, (ExteriorAlgebra.ι R) (b 0) * (ExteriorAlgebra.ι R) (b 1), (ExteriorAlgebra.ι R) (b 0) * (ExteriorAlgebra.ι R) (b 2), (ExteriorAlgebra.ι R) (b 1) * (ExteriorAlgebra.ι R) (b 2)] j

Evaluation of the ordered even-monomial coordinates.

noncomputable def TauCeti.spinSixTransvectionFirstVector {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} (P : SpinPolarizationData Q) (b : Module.Basis (Fin 3) R ↥P.W) (i j : Fin 4) : V

The first vector of the Eichler-transvection lift of an elementary matrix transvection on the even half-spin module.

theorem TauCeti.spinSixTransvectionFirstVector_apply {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} (P : SpinPolarizationData Q) (b : Module.Basis (Fin 3) R ↥P.W) (i j : Fin 4) : spinSixTransvectionFirstVector P b i j = !![0, ↑(P.dualVector b 0), ↑(P.dualVector b 0), ↑(P.dualVector b 1); ↑(b 1), 0, ↑(b 1), ↑(b 0); ↑(b 2), ↑(b 2), 0, ↑(b 0); ↑(b 2), ↑(b 2), ↑(b 1), 0] i j

Evaluation of the first vector of an elementary Spin-six transvection lift.

noncomputable def TauCeti.spinSixTransvectionSecondVector {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} (P : SpinPolarizationData Q) (b : Module.Basis (Fin 3) R ↥P.W) (i j : Fin 4) (c : R) : V

The second vector of the Eichler-transvection lift of an elementary matrix transvection on the even half-spin module.

theorem TauCeti.spinSixTransvectionSecondVector_apply {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} (P : SpinPolarizationData Q) (b : Module.Basis (Fin 3) R ↥P.W) (i j : Fin 4) (c : R) : spinSixTransvectionSecondVector P b i j c = !![0, ↑(c • P.dualVector b 1), ↑(c • P.dualVector b 2), ↑(c • P.dualVector b 2); ↑(c • b 0), 0, ↑(-c • P.dualVector b 2), ↑(c • P.dualVector b 2); ↑(c • b 0), ↑(-c • P.dualVector b 1), 0, ↑(-c • P.dualVector b 1); ↑(c • b 1), ↑(c • P.dualVector b 0), ↑(-c • P.dualVector b 0), 0] i j

Evaluation of the second vector of an elementary Spin-six transvection lift.

@[simp]

theorem TauCeti.spinSixTransvectionSecondVector_zero {R : Type u_1} [CommRing R] {V : Type u_2} [AddCommGroup V] [Module R V] {Q : QuadraticForm R V} (P : SpinPolarizationData Q) (b : Module.Basis (Fin 3) R ↥P.W) (i j : Fin 4) : spinSixTransvectionSecondVector P b i j 0 = 0

The second vector of an elementary Spin-six transvection lift vanishes at parameter zero.

Two vector actions on the even half of a three-generator exterior algebra

The generators anticommute; these instances put products in increasing order.

The four columns of the action of v₀ = e₀ + f₀ after a vector with parts x and d.

The four columns of the action of a vector with parts x and d after v₀ = e₀ + f₀.

The even half and its monomial basis

noncomputable def Module.Basis.spinSixEvenMonomialBasis {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module K M] (b : Basis (Fin 3) K M) {N : Submodule K (_root_.ExteriorAlgebra K M)} (hN : N = CliffordAlgebra.evenOdd 0 0) : Basis (Fin 4) K ↥N

The basis 1, e₀e₁, e₀e₂, e₁e₂ of the even half.

@[simp]

theorem Module.Basis.coe_spinSixEvenMonomialBasis {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module K M] (b : Basis (Fin 3) K M) {N : Submodule K (_root_.ExteriorAlgebra K M)} (hN : N = CliffordAlgebra.evenOdd 0 0) (j : Fin 4) : ↑((b.spinSixEvenMonomialBasis hN) j) = b.spinSixEvenMonomial j

The even-monomial basis has the prescribed exterior-algebra representatives.

The half-spin action of a polarized six-dimensional space

theorem TauCeti.det_spinPlusAction_spinGroupToEven {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) [Invertible 2] (hW : Module.finrank K ↥P.W = 3) (s : ↥(spinGroup Q)) : LinearMap.det ((spinPlusAction Q P hline) ((CliffordAlgebra.spinGroupToEven Q) s)) = 1

Spin acts on the even half-spin module with determinant one. For a polarization of a six-dimensional quadratic space, every element of Spin(Q) acts on S⁺ = ⋀ᵉᵛᵉⁿ W by an endomorphism of determinant one.

The Spin lifts of the elementary transvections

Creation pairs ι (c • e_a') * ι e_a move the vacuum 1 to e_a' ∧ e_a; annihilation pairs move e_a ∧ e_a' back to 1; mixed pairs exchange two of e₀e₁, e₀e₂, e₁e₂.

noncomputable def TauCeti.spinSixTransvectionLift {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (b : Module.Basis (Fin 3) K ↥P.W) [Invertible 2] {i j : Fin 4} (hij : i ≠ j) (c : K) : ↥(spinGroup Q)

The canonical Spin lift of an elementary transvection on the even half-spin module of a polarized six-dimensional quadratic space.

@[simp]

theorem TauCeti.spinSixTransvectionLift_zero {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (b : Module.Basis (Fin 3) K ↥P.W) [Invertible 2] {i j : Fin 4} (hij : i ≠ j) : spinSixTransvectionLift P hline b hij 0 = 1

The canonical lift of an elementary transvection with parameter zero is the identity.

@[simp]

theorem TauCeti.toMatrix_spinPlusAction_spinSixTransvectionLift {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (b : Module.Basis (Fin 3) K ↥P.W) [Invertible 2] {i j : Fin 4} (hij : i ≠ j) (c : K) : (LinearMap.toMatrix (b.spinSixEvenMonomialBasis ⋯) (b.spinSixEvenMonomialBasis ⋯)) ((spinPlusAction Q P hline) ((CliffordAlgebra.spinGroupToEven Q) (spinSixTransvectionLift P hline b hij c))) = Matrix.transvection i j c

The half-spin matrix of the canonical lift is the elementary transvection it lifts.

@[simp]

theorem TauCeti.spinVectorAction_spinSixTransvectionLift_apply {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (b : Module.Basis (Fin 3) K ↥P.W) [Invertible 2] {i j : Fin 4} (hij : i ≠ j) (c : K) (x : V) : (CliffordAlgebra.spinVectorAction Q (spinSixTransvectionLift P hline b hij c)) x = x + QuadraticMap.polar (⇑Q) x (spinSixTransvectionFirstVector P b i j) • spinSixTransvectionSecondVector P b i j c - QuadraticMap.polar (⇑Q) x (spinSixTransvectionSecondVector P b i j c) • spinSixTransvectionFirstVector P b i j - (Q (spinSixTransvectionSecondVector P b i j c) * QuadraticMap.polar (⇑Q) x (spinSixTransvectionFirstVector P b i j)) • spinSixTransvectionFirstVector P b i j

The vector action of the canonical lift is its defining Eichler transvection.

theorem TauCeti.exists_spinPlusAction_spinGroupToEven_eq_of_det_eq_one {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) [Invertible 2] (hW : Module.finrank K ↥P.W = 3) (f : Module.End K ↥(spinPlus Q P)) (hf : LinearMap.det f = 1) : ∃ (s : ↥(spinGroup Q)), (spinPlusAction Q P hline) ((CliffordAlgebra.spinGroupToEven Q) s) = f

Every determinant-one endomorphism of the even half-spin module comes from Spin. For a polarization of a six-dimensional quadratic space, the canonical Spin lifts of the Eichler transvections act on S⁺ as the elementary transvections of a basis, which generate the special linear group.

noncomputable def TauCeti.spinGroupEquivSpecialLinearGroupOfFinrankEqSix {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) : ↥(spinGroup Q) ≃* Matrix.SpecialLinearGroup (Fin 4) K

The Spin group of a polarized six-dimensional quadratic space is SL₄(K). A Spin element goes to the matrix of its action on the even half-spin module S⁺ in the basis TauCeti.spinPlusFinBasisOfFinrankEqSix; see TauCeti.coe_spinGroupEquivSpecialLinearGroupOfFinrankEqSix_apply. By TauCeti.coe_evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix_spinGroupToEvenUnitary_apply, this matrix is the first factor of the element's image in the matrix model of the even Clifford algebra, so on Spin the equivalence agrees with AlgEquiv.evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix. For three hyperbolic planes it is TauCeti.hyperbolicSixSpinEquivSpecialLinear.

@[simp]

theorem TauCeti.coe_spinGroupEquivSpecialLinearGroupOfFinrankEqSix_apply {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) (s : ↥(spinGroup Q)) : ↑((spinGroupEquivSpecialLinearGroupOfFinrankEqSix P hV) s) = (LinearMap.toMatrix (spinPlusFinBasisOfFinrankEqSix P hV) (spinPlusFinBasisOfFinrankEqSix P hV)) ((spinPlusAction Q P ⋯) ((CliffordAlgebra.spinGroupToEven Q) s))

The polarized Spin-to-special-linear equivalence sends a Spin element to the matrix of its action on the even half-spin module in the basis TauCeti.spinPlusFinBasisOfFinrankEqSix. As a simp lemma it has low priority, so that specialized rules such as TauCeti.coe_hyperbolicSixSpinEquivSpecialLinear_apply apply first.

Three hyperbolic planes

theorem TauCeti.mem_range_spinGroupToEvenUnitary_iff_det_hyperbolicSixEvenUnitaryEquivGeneralLinear (K : Type u_1) [Field K] [NeZero 2] (x : ↥(CliffordAlgebra.evenUnitaryGroup (splitEvenForm K 3))) : x ∈ (CliffordAlgebra.spinGroupToEvenUnitary (splitEvenForm K 3)).range ↔ (↑((hyperbolicSixEvenUnitaryEquivGeneralLinear K) x)).det = 1

Spin is the determinant-one part of the even unitary group of three hyperbolic planes. Under the identification U(C₀, σ) ≅ GL₄(K) by the first half-spin factor, an even unitary element lies in Spin(Q) exactly when its matrix has determinant one. For the isomorphism Spin(Q) ≅ SL₄(K) itself, see TauCeti.hyperbolicSixSpinEquivSpecialLinear.

@[reducible, inline]

noncomputable abbrev TauCeti.hyperbolicSixSpinEquivSpecialLinear (K : Type u_1) [Field K] [NeZero 2] : ↥(spinGroup (splitEvenForm K 3)) ≃* Matrix.SpecialLinearGroup (Fin 4) K

The Spin group of three hyperbolic planes is SL₄(K). This is TauCeti.spinGroupEquivSpecialLinearGroupOfFinrankEqSix for the canonical split polarization, so a Spin element goes to the matrix of its even half-spin action in TauCeti.spinSixHalfSpinStandardBasis. By TauCeti.coe_hyperbolicSixSpinEquivSpecialLinear_apply it is the restriction of TauCeti.hyperbolicSixEvenUnitaryEquivGeneralLinear to Spin, so Spin(Q) is the determinant-one subgroup of the reverse-unitary group U(C₀, σ) ≅ GL₄(K). Over ℚ, three hyperbolic planes give the split rational six-dimensional form, with U(C₀, σ) ≅ GL₄(ℚ) and Spin(Q) ≅ SL₄(ℚ).

@[simp]

theorem TauCeti.coe_hyperbolicSixSpinEquivSpecialLinear_apply (K : Type u_1) [Field K] [NeZero 2] (s : ↥(spinGroup (splitEvenForm K 3))) : ↑((hyperbolicSixSpinEquivSpecialLinear K) s) = ↑((hyperbolicSixEvenUnitaryEquivGeneralLinear K) ((CliffordAlgebra.spinGroupToEvenUnitary (splitEvenForm K 3)) s))

The Spin equivalence is the general linear equivalence of the even unitary group, read on Spin elements: the matrix of a Spin element is the first factor of its image in the matrix-product model TauCeti.hyperbolicSixEvenEquivMatrixProd. Compare TauCeti.coe_spinGroupEquivSpecialLinearGroupOfFinrankEqSix_apply, which gives the same matrix as the matrix of the even half-spin action in TauCeti.spinSixHalfSpinStandardBasis.

@[reducible, inline]

noncomputable abbrev TauCeti.spinSixHalfSpinMonomialBasis (K : Type u_1) [Field K] : Module.Basis (Fin 4) K ↥(spinPlus (splitEvenForm K 3) (splitEvenPolarization K 3))

The even half-spin basis made from the canonical exterior monomials.

@[reducible, inline]

noncomputable abbrev TauCeti.spinSixHalfSpinStandardBasis (K : Type u_1) [Field K] : Module.Basis (Fin 4) K ↥(spinPlus (splitEvenForm K 3) (splitEvenPolarization K 3))

The basis TauCeti.spinPlusFinBasisOfFinrankEqSix of the even half-spin module of three hyperbolic planes: TauCeti.hyperbolicSixSpinEquivSpecialLinear sends a Spin element to the matrix of its half-spin action in this basis. Unlike TauCeti.spinSixHalfSpinMonomialBasis it is not explicit; TauCeti.spinSixBasisChange_conjugate_spinPlusAction relates matrices in the two.

theorem TauCeti.spinSixBasisChange_conjugate_spinPlusAction (K : Type u_1) [Field K] [NeZero 2] (s : ↥(spinGroup (splitEvenForm K 3))) : (spinSixHalfSpinMonomialBasis K).toMatrix ⇑(spinSixHalfSpinStandardBasis K) * ↑((hyperbolicSixSpinEquivSpecialLinear K) s) * (spinSixHalfSpinStandardBasis K).toMatrix ⇑(spinSixHalfSpinMonomialBasis K) = (LinearMap.toMatrix (spinSixHalfSpinMonomialBasis K) (spinSixHalfSpinMonomialBasis K)) ((spinPlusAction (splitEvenForm K 3) (splitEvenPolarization K 3) ⋯) ((CliffordAlgebra.spinGroupToEven (splitEvenForm K 3)) s))

Conjugating the matrix of a Spin element under TauCeti.hyperbolicSixSpinEquivSpecialLinear by the change of basis between TauCeti.spinSixHalfSpinStandardBasis and TauCeti.spinSixHalfSpinMonomialBasis gives the matrix of its even half-spin action in the monomial basis 1, e₀e₁, e₀e₂, e₁e₂, where explicit matrices can be computed, as in TauCeti.spinSixBasisChange_transvection.

theorem TauCeti.spinSixBasisChange_transvection (K : Type u_1) [Field K] [NeZero 2] {i j : Fin 4} (hij : i ≠ j) (c : K) : (spinSixHalfSpinMonomialBasis K).toMatrix ⇑(spinSixHalfSpinStandardBasis K) * ↑((hyperbolicSixSpinEquivSpecialLinear K) (spinSixTransvectionLift (splitEvenPolarization K 3) ⋯ (splitEvenBasis K 3) hij c)) * (spinSixHalfSpinStandardBasis K).toMatrix ⇑(spinSixHalfSpinMonomialBasis K) = Matrix.transvection i j c

The conjugated fixed-coordinate matrix of a canonical Spin lift is the elementary transvection it lifts.

@[simp]

theorem TauCeti.spinGroupToEvenUnitary_hyperbolicSixSpinEquivSpecialLinear_symm_apply (K : Type u_1) [Field K] [NeZero 2] (A : Matrix.SpecialLinearGroup (Fin 4) K) : (CliffordAlgebra.spinGroupToEvenUnitary (splitEvenForm K 3)) ((hyperbolicSixSpinEquivSpecialLinear K).symm A) = (hyperbolicSixEvenUnitaryEquivGeneralLinear K).symm (Matrix.SpecialLinearGroup.toGL A)

The inverse Spin equivalence is the inverse general linear equivalence on determinant-one matrices.