The structure theorem for an even-dimensional Clifford algebra

A polarization of a quadratic space (V, Q) splits it as W ⊕ W' ⊕ L and makes the exterior algebra S = ⋀·W a module over CliffordAlgebra Q — the Fock model TauCeti.spinAction. That action is onto Module.End K S when W is finite free (TauCeti.spinAction_surjective): every endomorphism of S is a polynomial in the creation and annihilation operators.

This file proves the structure theorem, which is a dimension count. Deforming a quadratic form deforms the multiplication of its Clifford algebra and leaves the size alone, so finrank (CliffordAlgebra Q) = 2 ^ finrank V for every form (CliffordAlgebra.finrank_eq_two_pow), while finrank (Module.End K S) = (2 ^ finrank W) ^ 2. The dimension bookkeeping for a polarization, in TauCeti/RepresentationTheory/Spin/Polarization/Basic.lean, shows that in even dimension finrank W is exactly half of finrank V. The two dimensions therefore agree, and the surjection TauCeti.spinAction is forced to be an isomorphism:

TauCeti.SpinPolarizationData.cliffordEquivEnd : CliffordAlgebra Q ≃ₐ[K] Module.End K (⋀·W),

or, in a basis of S, TauCeti.SpinPolarizationData.cliffordEquivMatrix, the matrix algebra M_{2^l}(K) for finrank V = 2 * l. Since TauCeti.SpinPolarizationData.ofNondegenerate builds a polarization for every finite-dimensional nondegenerate quadratic space over a separably closed field of characteristic different from two, this specializes to the field-level statement CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul.

The direction of the argument is worth recording: the spin module is built first and the structure theorem is derived from it.

The same action identifies the even Clifford subalgebra with the product of the endomorphism algebras of the exterior-parity summands S⁺ and S⁻. Surjectivity onto that product is the substance: an endomorphism preserving both summands comes from a unique Clifford element, and its odd component must vanish because it both preserves and reverses parity.

The odd-dimensional case is not proved here. There finrank L = 1 and the count gives finrank (CliffordAlgebra Q) = 2 * (2 ^ l) ^ 2, so TauCeti.spinAction cannot be injective. Away from characteristic two the centre of the Clifford algebra of a nondegenerate odd-dimensional form is a quadratic étale algebra over K, so over a separably closed field it is K × K, the Clifford algebra is a product of two matrix algebras, and the action factors through one of the two central idempotents. Over a general field that centre can be a field, and then there is no such product decomposition. The idempotent half of that splitting is proved in TauCeti/LinearAlgebra/CliffordAlgebra/OddSplitting.lean: CliffordAlgebra.equivEvenProd splits the Clifford algebra of a central odd square root of one as two copies of its even subalgebra, and CliffordAlgebra.nonempty_algEquiv_even_prod_of_isSepClosed supplies that square root over a separably closed field. What is still separate work is identifying even Q for an odd-dimensional form with a matrix algebra, which is what would turn that product into the product of two matrix algebras.

Main definitions

• TauCeti.SpinPolarizationData.cliffordEquivEnd: the structure theorem in operator form, the Fock action promoted to an algebra isomorphism onto Module.End K (⋀·W).
• TauCeti.SpinPolarizationData.cliffordEquivMatrix: the same isomorphism read in a basis of the spinor module, onto Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) K.
• TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd: the even structure theorem in operator form, onto the product of the endomorphism algebras of S⁺ and S⁻.
• TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix: its product-of-matrix-algebras form.

Main results

• TauCeti.spinAction_bijective: the Fock action is faithful, hence bijective, in even dimension.
• TauCeti.evenSpinActionProd_surjective: the even Clifford action exhausts the paired endomorphism algebras of the half-spin summands.
• CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul: the matrix-algebra equivalence over a separably closed field.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §20.1, Lemma 20.9 and Proposition 20.15: the Clifford algebra of an even-dimensional space acts on ⋀·W through the full endomorphism algebra, the dimension count that makes the action an isomorphism, and the product decomposition of the even subalgebra on the two half-spin summands.
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.
• Spin-representations roadmap, Layer 1, "The even-dimensional case".

The structure theorem in even dimension

The count is finrank (CliffordAlgebra Q) = 2 ^ finrank V = 2 ^ (2 * l) = (2 ^ l) ^ 2 = finrank (Module.End K S), where the outer two equalities hold for every quadratic form on a finite free module and the inner one is the even-dimensional reading of the summand dimensions above. Injectivity of the Fock action is then forced by its surjectivity. Two is inverted throughout, as it already is in the dimension count CliffordAlgebra.finrank_eq_two_pow.

theorem TauCeti.SpinPolarizationData.finrank_exteriorAlgebra_W_of_finrank_eq_two_mul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] {l : ℕ} (hV : Module.finrank K V = 2 * l) : Module.finrank K (ExteriorAlgebra K ↥P.W) = 2 ^ l

The spinor module has dimension 2 ^ l when the polarized quadratic space has dimension 2 * l.

theorem TauCeti.SpinPolarizationData.finrank_cliffordAlgebra_eq_finrank_end {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] (h : Even (Module.finrank K V)) : Module.finrank K (CliffordAlgebra Q) = Module.finrank K (Module.End K (ExteriorAlgebra K ↥P.W))

The Clifford algebra and the operator algebra of the spinor module have equal dimension in even dimension: 2 ^ (2 * l) on the left, (2 ^ l) ^ 2 on the right. This is the dimension count that upgrades the surjection spinAction_surjective to an isomorphism.

theorem TauCeti.spinAction_injective {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] (h : Even (Module.finrank K V)) : Function.Injective ⇑(spinAction Q P)

The Fock action is faithful in even dimension. It is surjective onto an algebra of the same dimension, so it is injective.

theorem TauCeti.spinAction_bijective {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] (h : Even (Module.finrank K V)) : Function.Bijective ⇑(spinAction Q P)

The Fock action is bijective in even dimension: surjective for every polarization with a finite free isotropic summand, and injective by the dimension count.

noncomputable def TauCeti.SpinPolarizationData.cliffordEquivEnd {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] (h : Even (Module.finrank K V)) : CliffordAlgebra Q ≃ₐ[K] Module.End K (ExteriorAlgebra K ↥P.W)

The structure theorem in operator form: for an even-dimensional polarized quadratic space, the Fock action is an isomorphism of K-algebras from CliffordAlgebra Q onto the endomorphism algebra of the spinor module S = ⋀·W.

Equations

• P.cliffordEquivEnd h = AlgEquiv.ofBijective (TauCeti.spinAction Q P) ⋯

@[simp]

theorem TauCeti.SpinPolarizationData.cliffordEquivEnd_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] (h : Even (Module.finrank K V)) (x : CliffordAlgebra Q) : (P.cliffordEquivEnd h) x = (spinAction Q P) x

The operator form of the structure theorem is the Fock action itself.

noncomputable def TauCeti.SpinPolarizationData.cliffordEquivMatrix {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] {l : ℕ} (hV : Module.finrank K V = 2 * l) : CliffordAlgebra Q ≃ₐ[K] Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) K

The structure theorem: the Clifford algebra of a polarized quadratic space of dimension 2 * l is the matrix algebra M_{2^l}(K), read in a basis of the spinor module ⋀·W, which has dimension 2 ^ l.

Equations

• P.cliffordEquivMatrix hV = (P.cliffordEquivEnd ⋯).trans (TauCeti.Algebra.endAlgEquivMatrix K (ExteriorAlgebra K ↥P.W) ⋯)

@[simp]

theorem TauCeti.SpinPolarizationData.cliffordEquivMatrix_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] {l : ℕ} (hV : Module.finrank K V = 2 * l) (x : CliffordAlgebra Q) : (P.cliffordEquivMatrix hV) x = (Algebra.endAlgEquivMatrix K (ExteriorAlgebra K ↥P.W) ⋯) ((spinAction Q P) x)

The matrix form of the structure theorem is the Fock action followed by the chosen-basis identification of endomorphisms with matrices.

theorem TauCeti.SpinPolarizationData.isSimpleRing_cliffordAlgebra {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] [FiniteDimensional K V] (P : SpinPolarizationData Q) (h : Even (Module.finrank K V)) : IsSimpleRing (CliffordAlgebra Q)

An even-dimensional polarized Clifford algebra is a simple ring. The Fock action identifies it with the endomorphism algebra of its nonzero finite-dimensional spinor module.

theorem TauCeti.SpinPolarizationData.isCentral_cliffordAlgebra {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] [FiniteDimensional K V] (P : SpinPolarizationData Q) (h : Even (Module.finrank K V)) : Algebra.IsCentral K (CliffordAlgebra Q)

An even-dimensional polarized Clifford algebra has center the base field. The Fock action identifies it with the endomorphism algebra of its spinor module.

The even structure theorem

For an even-dimensional polarized quadratic space the Fock action is an isomorphism CliffordAlgebra Q ≃ₐ[K] Module.End K S. Under it the even subalgebra is carried onto the endomorphisms preserving the parity splitting S = S⁺ ⊕ S⁻, which is the product of the two endomorphism algebras; that is the content of this section.

theorem TauCeti.mem_even_of_map_spinPlus_le_of_map_spinMinus_le {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] (hline : P.line = ⊥) {x : CliffordAlgebra Q} (hplus : Submodule.map ((spinAction Q P) x) (spinPlus Q P) ≤ spinPlus Q P) (hminus : Submodule.map ((spinAction Q P) x) (spinMinus Q P) ≤ spinMinus Q P) : x ∈ CliffordAlgebra.even Q

A Clifford element whose action preserves both half-spin summands is even. Splitting it into an even and an odd part, the odd part acts by an operator that both preserves and reverses exterior parity, so it acts by zero; in even dimension the Fock action is faithful, so the odd part itself vanishes.

theorem TauCeti.exists_mem_even_spinAction_eq {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] (hline : P.line = ⊥) (f : Module.End K (ExteriorAlgebra K ↥P.W)) (hplus : Submodule.map f (spinPlus Q P) ≤ spinPlus Q P) (hminus : Submodule.map f (spinMinus Q P) ≤ spinMinus Q P) : ∃ (x : ↥(CliffordAlgebra.even Q)), (spinAction Q P) ↑x = f

An endomorphism of the spinor module preserving both half-spin summands is the action of an even Clifford element.

theorem TauCeti.evenSpinActionProd_injective {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] (hline : P.line = ⊥) : Function.Injective ⇑(evenSpinActionProd Q P hline)

The even subalgebra acts faithfully on the pair of half-spin summands. An even element acting by zero on both acts by zero on their sum, which is all of S, and in even dimension the Fock action is faithful.

theorem TauCeti.evenSpinActionProd_surjective {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] (hline : P.line = ⊥) : Function.Surjective ⇑(evenSpinActionProd Q P hline)

The even subalgebra exhausts the pair of endomorphism algebras. A pair of endomorphisms of the two summands assembles, along the splitting S = S⁺ ⊕ S⁻, into a parity-preserving endomorphism of S, and those are exactly the actions of even Clifford elements.

theorem TauCeti.spinPlusAction_surjective {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] (hline : P.line = ⊥) : Function.Surjective ⇑(spinPlusAction Q P hline)

The even Clifford action on S⁺ is onto its full endomorphism algebra.

theorem TauCeti.spinMinusAction_surjective {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] (hline : P.line = ⊥) : Function.Surjective ⇑(spinMinusAction Q P hline)

The even Clifford action on S⁻ is onto its full endomorphism algebra.

noncomputable def TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd {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] (hline : P.line = ⊥) : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Module.End K ↥(spinPlus Q P) × Module.End K ↥(spinMinus Q P)

The even structure theorem: for an even-dimensional polarized quadratic space the even Clifford subalgebra is the product of the endomorphism algebras of the two half-spin summands.

This is the even-subalgebra companion of TauCeti.SpinPolarizationData.cliffordEquivEnd. It gives the invariant-subspace dichotomy for both summands, which is simplicity for S⁺ and, when P.W ≠ ⊥, for S⁻; it also distinguishes their two even-Clifford actions.

Equations

• P.evenCliffordEquivProdEnd hline = AlgEquiv.ofBijective (TauCeti.evenSpinActionProd Q P hline) ⋯

@[simp]

theorem TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd_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] (hline : P.line = ⊥) (x : ↥(CliffordAlgebra.even Q)) : (P.evenCliffordEquivProdEnd hline) x = (evenSpinActionProd Q P hline) x

noncomputable def TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix {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] {l : ℕ} (hW : P.W ≠ ⊥) (hV : Module.finrank K V = 2 * l) : ↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix (Fin (2 ^ (l - 1))) (Fin (2 ^ (l - 1))) K × Matrix (Fin (2 ^ (l - 1))) (Fin (2 ^ (l - 1))) K

The matrix form of the even structure theorem: in dimension 2 * l, the even Clifford subalgebra is a product of two matrix algebras of size 2 ^ (l - 1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix_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] {l : ℕ} (hW : P.W ≠ ⊥) (hV : Module.finrank K V = 2 * l) (x : ↥(CliffordAlgebra.even Q)) : (P.evenCliffordEquivProdMatrix hW hV) x = ((Algebra.endAlgEquivMatrix K ↥(spinPlus Q P) ⋯) ((spinPlusAction Q P ⋯) x), (Algebra.endAlgEquivMatrix K ↥(spinMinus Q P) ⋯) ((spinMinusAction Q P ⋯) x))

The matrix form of the even structure theorem is the pair of half-spin actions, followed by the chosen-basis identifications of their endomorphism algebras with matrix algebras.

The field-level structure theorem

A finite-dimensional nondegenerate quadratic space over a separably closed field of characteristic different from two is polarized by TauCeti.SpinPolarizationData.ofNondegenerate, giving the split matrix-algebra statement.

theorem CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul {F : Type u} [Field F] [NeZero 2] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} [IsSepClosed F] {l : ℕ} (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank F V = 2 * l) : Nonempty (CliffordAlgebra Q ≃ₐ[F] Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F)

The structure theorem over a separably closed field: the Clifford algebra of a nondegenerate quadratic form on a 2l-dimensional space is the matrix algebra M_{2^l}(F).

The isomorphism is not canonical — it is read in a basis of the spinor module of a polarization, and neither the polarization nor the basis is unique — so the statement is Nonempty. The polarization-dependent isomorphism itself is TauCeti.SpinPolarizationData.cliffordEquivMatrix.