Documentation

TauCeti.RepresentationTheory.Spin.OddStructure

The structure theorem for an odd-dimensional Clifford algebra #

Over a separably closed field of characteristic not two, the Clifford algebra of a nondegenerate quadratic form on a space of dimension 2 * l + 1 is a product of two matrix algebras,

CliffordAlgebra Q ≃ₐ[F] M_{2^l}(F) × M_{2^l}(F).

Two results already in place bracket this statement, and the file supplies what joins them. The volume element of an orthogonal basis of odd length is central, odd, and squares to a nonzero scalar, so after rescaling it splits the algebra as two copies of its even subalgebra (CliffordAlgebra.nonempty_algEquiv_even_prod_of_odd_finrank); and the Fock action of a polarization is onto the endomorphism algebra of the spinor module S = ⋀·W (TauCeti.spinAction_surjective), which in dimension 2 * l + 1 has dimension 2 ^ l. What was missing was the identification of the even subalgebra itself with M_{2^l}(F), and that is the substance here.

The argument avoids reducing an odd-dimensional form to an even-dimensional one. Write A = even Q, so that the splitting is a surjection A × A ↠ M_{2^l}(F) obtained by following it with the Fock action. The image of (1, 0) is a central idempotent of a simple ring, hence 0 or 1 (TauCeti.centralIdempotents_eq_pair), and in either case one of the two coordinate maps a ↦ φ (a, 0), a ↦ φ (0, a) is already a surjective algebra map A →ₐ[F] M_{2^l}(F): that is AlgHom.exists_algHom_surjective_of_prod. A dimension count closes it. The even subalgebra has half the dimension of the whole (CliffordAlgebra.finrank_even), so dim A = 2 ^ (2 * l + 1 - 1) = 2 ^ l · 2 ^ l is the dimension of the target and the surjection is injective as well.

The splitting itself is general Clifford-algebra theory and lives with the rest of it, in TauCeti/LinearAlgebra/CliffordAlgebra/OddSplitting.lean.

The isomorphisms are not canonical — they depend on a choice of orthogonal basis, of polarization, and of a basis of the spinor module — so the statements are Nonempty, as the even-dimensional CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul is.

Once a polarization is fixed there is a canonical isomorphism to be had, and the last section records it. Only the basis of the spinor module was arbitrary above, so dropping it leaves the Fock action itself: TauCeti.evenSpinAction is a bijection from even Q onto Module.End F (⋀·W). That needs neither the matrix identification nor a separably closed field. The whole Fock action is onto (TauCeti.spinAction_surjective), and in odd dimension the even half already reaches as far: the volume element ω is central, so its image commutes with all of Module.End F (⋀·W) and is a scalar, and ω is odd with ω² = c ≠ 0, so each generator is ι v = c⁻¹ (ι v * ω) * ω with ι v * ω even. A dimension count then makes the surjection injective. That statement, TauCeti.SpinPolarizationData.evenCliffordEquivEnd, is the odd-dimensional companion of the even TauCeti.SpinPolarizationData.cliffordEquivEnd, one grade down: in even dimension the whole Clifford algebra is Module.End F (⋀·W), in odd dimension only its even half is, the whole algebra being two copies of that half.

Main results #

References #

The dimension count in odd dimension #

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

The spinor module has dimension 2 ^ l when the polarized quadratic space has dimension 2 * l + 1. The isotropic summand has dimension l in odd dimension as well as in even dimension, the extra dimension being taken up by the anisotropic remainder, so the two parities give spinor modules of the same size.

source
theorem TauCeti.SpinPolarizationData.finrank_even_eq_finrank_end_of_odd_finrank {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) [Invertible 2] (hodd : Odd (Module.finrank F V)) :
Module.finrank F ↥(CliffordAlgebra.even Q) = Module.finrank F (Module.End F (ExteriorAlgebra F ↥P.W))

The even Clifford subalgebra and the operator algebra of the spinor module have equal dimension in odd dimension: writing finrank F V = 2 * l + 1, that is 2 ^ (2 * l + 1 - 1) on the left and (2 ^ l) ^ 2 on the right.

This is the odd-dimensional analogue of TauCeti.SpinPolarizationData.finrank_cliffordAlgebra_eq_finrank_end, and the shift of one power of two is exactly the difference between the two parities: in even dimension the whole Clifford algebra matches the operator algebra of ⋀·W, while in odd dimension only its even half does.

The structure theorem in odd dimension #

source
theorem CliffordAlgebra.nonempty_algEquiv_even_matrix_of_finrank_eq_two_mul_add_one {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 + 1) :
Nonempty (↥(even Q) ≃ₐ[F] Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F)

The even subalgebra of an odd-dimensional Clifford algebra is a matrix algebra. The Fock action of a polarization is onto the endomorphism algebra of the spinor module, of dimension 2 ^ l; composed with the two-block splitting it becomes a surjection from a product of two copies of even Q, which AlgHom.exists_algHom_surjective_of_prod turns into a surjection out of a single copy. Both sides have dimension 2 ^ l · 2 ^ l — the even subalgebra by CliffordAlgebra.finrank_even — so that surjection is an isomorphism.

source
theorem CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one {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 + 1) :
Nonempty (CliffordAlgebra Q ≃ₐ[F] Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F × Matrix (Fin (2 ^ l)) (Fin (2 ^ l)) F)

The structure theorem in odd dimension: over a separably closed field of characteristic not two, the Clifford algebra of a nondegenerate quadratic form on a space of dimension 2 * l + 1 is the product of two copies of the matrix algebra M_{2^l}(F).

This is the odd-dimensional companion of CliffordAlgebra.nonempty_algEquiv_matrix_of_finrank_eq_two_mul, and the two blocks are not an artefact of the proof: the product displayed here has (1, 0) as a central idempotent other than 0 and 1, so the algebra is not simple, whereas in even dimension it is (TauCeti.SpinPolarizationData.isSimpleRing_cliffordAlgebra).

The odd structure theorem in operator form #

The matrix identification above is not canonical: it depends on a basis of the spinor module. The Fock action itself is canonical once a polarization is chosen, and it identifies the even subalgebra with the operator algebra of the spinor module directly, over any field of characteristic not two: the polarization data carries the nondegeneracy, and the volume element does the rest without being normalized to a square root of one.

source
theorem TauCeti.evenSpinAction_surjective {F : Type u} [Field F] [NeZero 2] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) (hodd : Odd (Module.finrank F V)) :
Function.Surjective ⇑(evenSpinAction Q P)

The even Clifford action on the spinor module is onto in odd dimension. The whole Fock action is onto by TauCeti.spinAction_surjective, and in odd dimension the even half already reaches everything the odd half does: the volume element ω of an orthogonal basis is central, odd, and squares to a nonzero scalar, so its image is a scalar operator, and every generator factors as ι v = c⁻¹ (ι v * ω) * ω with ι v * ω even.

This is the sharp form of the odd-dimensional structure theorem: unlike the whole Clifford algebra, which needs both spinor modules to act faithfully, the even subalgebra already sees all of Module.End F (⋀·W). Neither nondegeneracy nor a separably closed field is assumed: the polarization data carries the first (TauCeti.SpinPolarizationData.nondegenerate) and the argument never normalizes ω, which is what the second was for.

source
theorem TauCeti.evenSpinAction_injective {F : Type u} [Field F] [NeZero 2] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) (hodd : Odd (Module.finrank F V)) :
Function.Injective ⇑(evenSpinAction Q P)

The even Clifford action on the spinor module is faithful in odd dimension. It is onto an algebra of the same dimension, so it is injective.

source
noncomputable def TauCeti.SpinPolarizationData.evenCliffordEquivEnd {F : Type u} [Field F] [NeZero 2] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) (hodd : Odd (Module.finrank F V)) :
↥(CliffordAlgebra.even Q) ≃ₐ[F] Module.End F (ExteriorAlgebra F ↥P.W)

The odd structure theorem in operator form: for a polarized quadratic space of odd dimension over a field of characteristic not two, the Fock action is an isomorphism of F-algebras from the even Clifford subalgebra onto the endomorphism algebra of the spinor module S = ⋀·W.

This is the odd-dimensional companion of TauCeti.SpinPolarizationData.cliffordEquivEnd, one grade down: there the whole algebra is Module.End F S, here only its even half is, the whole algebra being two copies of it.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.evenCliffordEquivEnd_apply {F : Type u} [Field F] [NeZero 2] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) (hodd : Odd (Module.finrank F V)) (x : ↥(CliffordAlgebra.even Q)) :
    (P.evenCliffordEquivEnd hodd) x = (spinAction Q P) ↑x

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