The even Clifford algebra in odd dimension is central simple

For a regular quadratic form in odd dimension over a field of characteristic different from two, its even Clifford algebra is central and a simple ring. With finite dimensionality, inherited from the full Clifford algebra, this is the odd-dimensional algebra whose Brauer class defines the Clifford invariant.

The reduction uses diagonalization and TauCeti.CliffordAlgebra.evenProdSMulSqEquiv: splitting off a nondegenerate line identifies the even algebra with the full Clifford algebra of a regular form in one lower dimension, which is central simple by the even-dimensional theorem. No square root or extension of the base field is needed for this reduction.

Main results

• TauCeti.CliffordAlgebra.exists_reversalEquiv_even_of_finrank_pos: the dimension-reduction equivalence carries reversal to Clifford conjugation.
• TauCeti.CliffordAlgebra.exists_nonempty_algEquiv_even_of_finrank_pos: in positive dimension, the even algebra is isomorphic to the Clifford algebra of a regular form in one lower dimension.
• TauCeti.CliffordAlgebra.exists_nonempty_algEquiv_even_of_odd_finrank: the even algebra is isomorphic to the Clifford algebra of a regular form of even dimension.
• TauCeti.CliffordAlgebra.isSimpleRing_even_of_odd_finrank: the even algebra is a simple ring.
• TauCeti.CliffordAlgebra.isCentral_even_of_odd_finrank: the even algebra is central.
• TauCeti.CliffordAlgebra.deg_even_of_odd_finrank: its degree is 2 ^ ((finrank K V - 1) / 2).
• TauCeti.CliffordAlgebra.deg_even_of_finrank_eq_five: in dimension five its degree is four.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Theorem V.2.5.

theorem TauCeti.CliffordAlgebra.exists_reversalEquiv_even_of_finrank_pos {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hV : 0 < Module.finrank K V) : ∃ (n : ℕ) (P : QuadraticForm K (Fin n → K)), QuadraticMap.Nondegenerate ∧ n + 1 = Module.finrank K V ∧ ∃ (e : ↥(CliffordAlgebra.even Q) ≃ₐ[K] CliffordAlgebra P), ∀ (x : ↥(CliffordAlgebra.even Q)), e ((CliffordAlgebra.reverseEven Q) x) = star (e x)

In positive dimension, dimension reduction carries the even Clifford algebra to a regular full Clifford algebra in one lower dimension and carries reversal to Clifford conjugation.

theorem TauCeti.CliffordAlgebra.exists_nonempty_algEquiv_even_of_finrank_pos {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hV : 0 < Module.finrank K V) : ∃ (n : ℕ) (P : QuadraticForm K (Fin n → K)), QuadraticMap.Nondegenerate ∧ n + 1 = Module.finrank K V ∧ Nonempty (↥(CliffordAlgebra.even Q) ≃ₐ[K] CliffordAlgebra P)

In positive dimension, the even Clifford algebra of a regular quadratic space is isomorphic to the full Clifford algebra of a regular form in one lower dimension: splitting off a line ⟨a⟩ from Q ≅ ⟨a⟩ ⊥ P gives even Q ≃ₐ[K] CliffordAlgebra (-a⁻¹ • P). The new form lives on Fin n → K, so the isomorphism also moves the algebra into the universe of K.

theorem TauCeti.CliffordAlgebra.exists_nonempty_algEquiv_even_of_odd_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hV : Odd (Module.finrank K V)) : ∃ (n : ℕ) (P : QuadraticForm K (Fin n → K)), QuadraticMap.Nondegenerate ∧ Even n ∧ Nonempty (↥(CliffordAlgebra.even Q) ≃ₐ[K] CliffordAlgebra P)

The even Clifford algebra of a regular odd-dimensional quadratic space is isomorphic to the full Clifford algebra of a regular form in one lower, hence even, dimension; this is TauCeti.CliffordAlgebra.exists_nonempty_algEquiv_even_of_finrank_pos read in odd dimension.

theorem TauCeti.CliffordAlgebra.isSimpleRing_even_of_odd_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hV : Odd (Module.finrank K V)) : IsSimpleRing ↥(CliffordAlgebra.even Q)

The even Clifford algebra of a regular odd-dimensional quadratic space is a simple ring. Together with centrality and inherited finite dimensionality, this defines its Brauer class.

theorem TauCeti.CliffordAlgebra.isCentral_even_of_odd_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hV : Odd (Module.finrank K V)) : Algebra.IsCentral K ↥(CliffordAlgebra.even Q)

The even Clifford algebra of a regular odd-dimensional quadratic space is central (Lam V.2.5): its centre is the base field, although the centre of the full Clifford algebra is two-dimensional in odd dimension.

theorem TauCeti.CliffordAlgebra.deg_even_of_odd_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hV : Odd (Module.finrank K V)) : Algebra.deg K ↥(CliffordAlgebra.even Q) = 2 ^ ((Module.finrank K V - 1) / 2)

The degree of the even Clifford algebra in odd dimension. For a quadratic form on a space of dimension 2m + 1, the even Clifford algebra has dimension 2 ^ (2m), hence degree 2 ^ m. When the form is regular, the preceding results also make this algebra central simple.

theorem TauCeti.CliffordAlgebra.deg_even_of_finrank_eq_five {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] {Q : QuadraticForm K V} (hV : Module.finrank K V = 5) : Algebra.deg K ↥(CliffordAlgebra.even Q) = 4

A five-dimensional even Clifford algebra has degree four. For a regular form, this is the algebra-size part of the description of Spin₅ as the unitary group of a degree-four central simple algebra with its canonical symplectic involution.