The even unitary group of a split six-dimensional quadratic space

A matrix-product model of the even Clifford algebra of a nondegenerate six-dimensional form identifies its reverse-unitary group with the general linear group of either matrix factor. Reversal exchanges the two central idempotents, so the second component of a unitary element is determined by the inverse of its first component. This differs from dimension four, where reversal preserves both factors and imposes determinant one in each.

The canonical polarization of the hyperbolic space splitEvenForm K 3 supplies such a model through TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix. Its matrix factors have size four. In particular, the even unitary group of three rational hyperbolic planes is GL₄(ℚ). This file concerns the even unitary carrier; its Spin subgroup is the subgroup of determinant-one matrices, by TauCeti.hyperbolicSixSpinEquivSpecialLinear.

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §15.
• The half-spin matrix-product structure theorem in TauCeti/RepresentationTheory/Spin/Structure.lean.

@[simp]

theorem AlgEquiv.map_reverseEven_symm_one_zero_of_finrank_eq_six {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : Type w} [Fintype n] [DecidableEq n] [Nonempty n] [Invertible 2] (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix n n K × Matrix n n K) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 6) : e ((CliffordAlgebra.reverseEven Q) (e.symm (1, 0))) = (0, 1)

In a matrix-product model of a nondegenerate six-dimensional even Clifford algebra, reversal exchanges the two central idempotents.

noncomputable def AlgEquiv.evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : Type w} [Fintype n] [DecidableEq n] [Nonempty n] [Invertible 2] (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix n n K × Matrix n n K) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 6) : ↥(CliffordAlgebra.evenUnitaryGroup Q) ≃* GL n K

Projecting to the first matrix factor identifies the reverse-unitary group of a nondegenerate six-dimensional even Clifford algebra with the general linear group. The matrix model is part of the data; reversal determines the inverse map uniquely.

@[simp]

theorem AlgEquiv.coe_evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : Type w} [Fintype n] [DecidableEq n] [Nonempty n] [Invertible 2] (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix n n K × Matrix n n K) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 6) (x : ↥(CliffordAlgebra.evenUnitaryGroup Q)) : ↑((e.evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix hQ hV) x) = (e ((CliffordAlgebra.evenUnitaryGroupEvenPart Q) x)).1

The general linear equivalence evaluates the first factor of the chosen even-Clifford model.

@[simp]

theorem AlgEquiv.fst_evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix_symm_apply_evenPart {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : Type w} [Fintype n] [DecidableEq n] [Nonempty n] [Invertible 2] (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix n n K × Matrix n n K) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 6) (u : GL n K) : (e ((CliffordAlgebra.evenUnitaryGroupEvenPart Q) ((e.evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix hQ hV).symm u))).1 = ↑u

The first matrix component of the inverse unitary transport is the given general linear matrix. This reconstruction rule runs before simplifying the full inverse Clifford value.

@[simp]

theorem AlgEquiv.evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix_symm_apply_evenPart {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {n : Type w} [Fintype n] [DecidableEq n] [Nonempty n] [Invertible 2] (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix n n K × Matrix n n K) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 6) (u : GL n K) : (CliffordAlgebra.evenUnitaryGroupEvenPart Q) ((e.evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix hQ hV).symm u) = e.symm ((↑u, 0) + e ((CliffordAlgebra.reverseEven Q) (e.symm (↑u⁻¹, 0))))

The inverse general linear equivalence has even Clifford value obtained from the first matrix and the reversed inverse matrix in the other factor.

theorem TauCeti.SpinPolarizationData.line_eq_bot_of_finrank_eq_six {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) : P.line = ⊥

The remainder line of a polarization of a six-dimensional quadratic space vanishes.

theorem TauCeti.SpinPolarizationData.finrank_W_eq_three_of_finrank_eq_six {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) : Module.finrank K ↥P.W = 3

A polarization of a six-dimensional quadratic space has a three-dimensional isotropic summand W.

theorem TauCeti.SpinPolarizationData.W_ne_bot_of_finrank_eq_six {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) : P.W ≠ ⊥

A polarization of a six-dimensional quadratic space has a nonzero isotropic summand W.

theorem TauCeti.finrank_spinPlus_eq_four_of_finrank_eq_six {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) : Module.finrank K ↥(spinPlus Q P) = 4

The even half-spin module of a polarized six-dimensional quadratic space has dimension four.

noncomputable def TauCeti.spinPlusFinBasisOfFinrankEqSix {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hV : Module.finrank K V = 6) : Module.Basis (Fin 4) K ↥(spinPlus Q P)

The basis Module.finBasisOfFinrankEq of the even half-spin module of a polarized six-dimensional quadratic space. It is the basis in which Algebra.endAlgEquivMatrix computes the first factor of TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix.

theorem TauCeti.spinPlusFinBasisOfFinrankEqSix_def {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K ↥(spinPlus Q P)] (hV : Module.finrank K V = 6) : spinPlusFinBasisOfFinrankEqSix P hV = Module.finBasisOfFinrankEq K ↥(spinPlus Q P) ⋯

TauCeti.spinPlusFinBasisOfFinrankEqSix is the basis Module.finBasisOfFinrankEq for the dimension count TauCeti.finrank_spinPlus_eq_four_of_finrank_eq_six.

theorem TauCeti.coe_evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix_spinGroupToEvenUnitary_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Invertible 2] [FiniteDimensional K V] (hV : Module.finrank K V = 6) (s : ↥(spinGroup Q)) : ↑(((P.evenCliffordEquivProdMatrix ⋯ hV).evenUnitaryGroupEquivGeneralLinearOfFinrankEqSix ⋯ hV) ((CliffordAlgebra.spinGroupToEvenUnitary Q) s)) = (LinearMap.toMatrix (spinPlusFinBasisOfFinrankEqSix P hV) (spinPlusFinBasisOfFinrankEqSix P hV)) ((spinPlusAction Q P ⋯) ((CliffordAlgebra.spinGroupToEven Q) s))

The first matrix factor of a polarized six-dimensional Spin element is the matrix of its even half-spin action in the basis TauCeti.spinPlusFinBasisOfFinrankEqSix.

@[instance_reducible]

def TauCeti.hyperbolicSixInvertibleTwo (K : Type u) [Field K] [NeZero 2] : Invertible 2

The invertibility witness used by the characteristic-not-two Clifford APIs.

noncomputable def TauCeti.hyperbolicSixEvenEquivMatrixProd (K : Type u) [Field K] : ↥(CliffordAlgebra.even (splitEvenForm K 3)) ≃ₐ[K] Matrix (Fin 4) (Fin 4) K × Matrix (Fin 4) (Fin 4) K

The half-spin matrix-product model of the even Clifford algebra of three hyperbolic planes.

theorem TauCeti.hyperbolicSixEvenEquivMatrixProd_apply (K : Type u) [Field K] (x : ↥(CliffordAlgebra.even (splitEvenForm K 3))) : (hyperbolicSixEvenEquivMatrixProd K) x = ((splitEvenPolarization K 3).evenCliffordEquivProdMatrix ⋯ ⋯) x

The hyperbolic matrix-product model is the model of the canonical split polarization.

noncomputable def TauCeti.hyperbolicSixEvenUnitaryEquivGeneralLinear (K : Type u) [Field K] [NeZero 2] : ↥(CliffordAlgebra.evenUnitaryGroup (splitEvenForm K 3)) ≃* GL (Fin 4) K

The even unitary group of three hyperbolic planes is the four-dimensional general linear group. In particular, specializing K to ℚ gives the split rational six-dimensional model.

@[simp]

theorem TauCeti.coe_hyperbolicSixEvenUnitaryEquivGeneralLinear_apply (K : Type u) [Field K] [NeZero 2] (x : ↥(CliffordAlgebra.evenUnitaryGroup (splitEvenForm K 3))) : ↑((hyperbolicSixEvenUnitaryEquivGeneralLinear K) x) = ((hyperbolicSixEvenEquivMatrixProd K) ((CliffordAlgebra.evenUnitaryGroupEvenPart (splitEvenForm K 3)) x)).1

The hyperbolic general linear equivalence is the first half-spin matrix component.

@[simp]

theorem TauCeti.fst_hyperbolicSixEvenUnitaryEquivGeneralLinear_symm_apply_evenPart (K : Type u) [Field K] [NeZero 2] (u : GL (Fin 4) K) : ((hyperbolicSixEvenEquivMatrixProd K) ((CliffordAlgebra.evenUnitaryGroupEvenPart (splitEvenForm K 3)) ((hyperbolicSixEvenUnitaryEquivGeneralLinear K).symm u))).1 = ↑u

Reconstructing a hyperbolic even unitary element recovers the given first matrix component. The rule precedes simplification of the full inverse Clifford value.

@[simp]

theorem TauCeti.hyperbolicSixEvenUnitaryEquivGeneralLinear_symm_apply_evenPart (K : Type u) [Field K] [NeZero 2] (u : GL (Fin 4) K) : (CliffordAlgebra.evenUnitaryGroupEvenPart (splitEvenForm K 3)) ((hyperbolicSixEvenUnitaryEquivGeneralLinear K).symm u) = (hyperbolicSixEvenEquivMatrixProd K).symm ((↑u, 0) + (hyperbolicSixEvenEquivMatrixProd K) ((CliffordAlgebra.reverseEven (splitEvenForm K 3)) ((hyperbolicSixEvenEquivMatrixProd K).symm (↑u⁻¹, 0))))

The inverse hyperbolic equivalence reconstructs the even Clifford value using reversal and the inverse of the given general linear matrix.