The weights of the spinor module

A polarization of a quadratic space (V, Q) splits it as W ⊕ W' ⊕ L with W and W' isotropic and in perfect QuadraticMap.polar-pairing, and TauCeti.spinAction makes the exterior algebra S = ⋀·W a module over CliffordAlgebra Q. This file diagonalizes S.

Fix a basis w : ι → W. The pairing turns each coordinate functional of that basis into a vector w' i of W', and the Clifford bivector

H i = bivector Q (w i) (w' i) = ⅟2 (ι (w i) * ι (w' i) - ι (w' i) * ι (w i))

is a quadratic element of the Clifford algebra, so it lies in the Lie subalgebra CliffordAlgebra.quadraticLieSubalgebra Q that realizes 𝔰𝔬(V, Q). These elements commute (TauCeti.SpinPolarizationData.lie_diagonalBivector_diagonalBivector), and they act diagonally on the exterior basis of S: on the basis vector indexed by a finite set s of indices — the wedge of the w i for i ∈ s — the element H i acts by

spinWeight K s i = if i ∈ s then ⅟2 else -⅟2.

So the weight of that basis vector is the half-integer sign vector ½(±1, …, ±1), the signs recording which basis vectors of W occur. Half-integrality is recorded literally, in TauCeti.spinWeight_add_self_of_mem and TauCeti.spinWeight_add_self_of_notMem: twice a weight is ±1.

Two facts pin the diagonalization down. The simultaneous eigenspace at the eigenvalue tuple spinWeight K s is exactly the line spanned by the corresponding exterior basis vector (TauCeti.spinWeightSpace_spinWeight), and, over a ring without zero divisors, every other tuple of eigenvalues has zero simultaneous eigenspace (TauCeti.spinWeightSpace_eq_bot_of_notMem_range). Hence, for a finite index type, the tuples that do occur are exactly the sign vectors (TauCeti.range_spinWeight), and, when K is nontrivial, there are 2 ^ l of them on an index type of cardinality l (TauCeti.ncard_range_spinWeight); their lines exhaust S (TauCeti.iSup_spinWeightSpace_eq_top).

The cancellation behind the first of those needs no field: two distinct sign vectors differ in some coordinate by ±1, a unit, so a coefficient annihilated by that difference vanishes over any commutative ring in which 2 is invertible.

What is deliberately absent: the elements H i are only shown to commute, and no Lie subalgebra of CliffordAlgebra.quadraticLieSubalgebra Q is exhibited as a Cartan subalgebra, so "weight" below always means a tuple of simultaneous eigenvalues for the indexed family H, not a linear character of a Cartan subalgebra. No ordering of ι is used to single out a Borel, so no weight is called highest here; the elements H i are not compared with a matrix model of 𝔰𝔬(2l + 1) or 𝔰𝔬(2l); and the abstract Bₗ/Dₗ root data are not mentioned. Those comparisons are the rest of the layer this file opens.

Main definitions

• TauCeti.SpinPolarizationData.diagonalBivector: the Clifford bivector H i of a basis vector of W and its dual vector in W'.
• TauCeti.spinWeight: the sign vector ½(±1, …, ±1) attached to a finite set of indices.
• TauCeti.spinWeightSpace: the simultaneous eigenspace of the elements H i at a prescribed tuple of eigenvalues.

Main results

• TauCeti.SpinPolarizationData.lie_diagonalBivector_diagonalBivector: the diagonal bivectors commute.
• TauCeti.SpinPolarizationData.spinAction_diagonalBivector_basis: the diagonal bivectors act diagonally on the exterior basis, by ⅟2 or -⅟2.
• TauCeti.SpinPolarizationData.spinAction_two_smul_diagonalBivector_basis and TauCeti.SpinPolarizationData.spinAction_diagonalBivector_sub_diagonalBivector_basis: twice a diagonal bivector acts by ±1, and a difference of two of them by a difference of two weights. These are the two combinations that a coroot of an orthogonal Lie algebra realizes.
• TauCeti.spinWeightSpace_spinWeight: each weight space is the line spanned by its exterior basis vector.
• TauCeti.spinWeightSpace_eq_bot_of_notMem_range and TauCeti.spinWeightSpace_ne_bot_iff: no other tuple of eigenvalues occurs.
• TauCeti.iSup_spinWeightSpace_eq_top: the weight spaces exhaust the spinor module.
• TauCeti.range_spinWeight: for a finite index type the weights are exactly the sign vectors, and, when K is nontrivial, TauCeti.ncard_range_spinWeight counts them: there are 2 ^ l of them on an index type of cardinality l.
• TauCeti.ncard_image_spinWeight_even and TauCeti.ncard_image_spinWeight_odd: on a nonempty index type the two parities of sign vector are equinumerous, 2 ^ (l - 1) each. On the empty index type they are not: the only sign vector is the empty one, which is even, so the even count is 2 ^ (0 - 1) = 1 and the odd one is 0, which is why the odd theorem asks l > 0. These are the weights of the two half-spin summands; the identification is TauCeti/RepresentationTheory/Spin/HalfSpin/Weight.lean.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §20.1: the weights ½(±1, …, ±1) of the spin module S = ⋀·W.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §5.
• Spin-representations roadmap, Layer 5, "Weights of the spin module".

The sign-vector weights

def TauCeti.spinWeight (K : Type u) [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] (s : Finset ι) (i : ι) : K

The weight of the exterior basis vector indexed by a finite set s: the half-integer sign vector ½(±1, …, ±1) whose i-th sign records whether i occurs in s.

Equations

• TauCeti.spinWeight K s i = if i ∈ s then ⅟2 else -⅟2

theorem TauCeti.spinWeight_apply {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] (s : Finset ι) (i : ι) : spinWeight K s i = if i ∈ s then ⅟2 else -⅟2

@[simp]

theorem TauCeti.spinWeight_of_mem {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) : spinWeight K s i = ⅟2

@[simp]

theorem TauCeti.spinWeight_of_notMem {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∉ s) : spinWeight K s i = -⅟2

theorem TauCeti.spinWeight_add_self_of_mem {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) : spinWeight K s i + spinWeight K s i = 1

The weights are half-integral: twice the weight at an occupied index is 1.

theorem TauCeti.spinWeight_add_self_of_notMem {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∉ s) : spinWeight K s i + spinWeight K s i = -1

The weights are half-integral: twice the weight at a vacant index is -1.

theorem TauCeti.exists_spinWeight_sub_eq_one_or_neg_one {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] {s t : Finset ι} (h : s ≠ t) : ∃ (i : ι), spinWeight K s i - spinWeight K t i = 1 ∨ spinWeight K s i - spinWeight K t i = -1

Distinct index sets have weights that differ by a unit in some coordinate. This is the cancellation making the weight spaces one-dimensional over an arbitrary commutative ring.

theorem TauCeti.spinWeight_injective {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] [Nontrivial K] : Function.Injective (spinWeight K)

Distinct index sets carry distinct weights.

theorem TauCeti.range_spinWeight {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] [Finite ι] : Set.range (spinWeight K) = {χ : ι → K | ∀ (i : ι), χ i = ⅟2 ∨ χ i = -⅟2}

The values of TauCeti.spinWeight are exactly the sign vectors ½(±1, …, ±1), when the index type is finite. Together with TauCeti.spinWeightSpace_ne_bot_iff this says the tuples of eigenvalues occurring in the spinor module are exactly those sign vectors; TauCeti.ncard_range_spinWeight counts them.

theorem TauCeti.ncard_range_spinWeight {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] [Finite ι] [Nontrivial K] : (Set.range (spinWeight K)).ncard = 2 ^ Nat.card ι

There are exactly 2 ^ l sign vectors on a finite index type of cardinality l: distinct index sets carry distinct weights, and there are 2 ^ l index sets.

theorem TauCeti.ncard_image_spinWeight_even {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] [Finite ι] [Nontrivial K] : (spinWeight K '' {s : Finset ι | Even s.card}).ncard = 2 ^ (Nat.card ι - 1)

The sign vectors with an even number of + signs number 2 ^ (l - 1) on an index type of cardinality l. For l > 0 that is half of the 2 ^ l sign vectors of TauCeti.ncard_range_spinWeight, the odd ones of TauCeti.ncard_image_spinWeight_odd being the other half; for l = 0 it is no half but the single empty sign vector, which is even, and 2 ^ (0 - 1) = 1 counts it. These are the weights of the even half-spin summand, by TauCeti.setOf_spinWeightSpace_ne_bot_and_le_spinPlus_eq_image_spinWeight_even.

theorem TauCeti.ncard_image_spinWeight_odd {K : Type u} [CommRing K] [Invertible 2] {ι : Type w} [DecidableEq ι] [Finite ι] [Nonempty ι] [Nontrivial K] : (spinWeight K '' {s : Finset ι | Odd s.card}).ncard = 2 ^ (Nat.card ι - 1)

The sign vectors with an odd number of + signs number 2 ^ (l - 1), the other half of TauCeti.ncard_image_spinWeight_even, on a nonempty index type: the empty index type has no sign vector of odd parity. These are the weights of the odd half-spin summand, by TauCeti.setOf_spinWeightSpace_ne_bot_and_le_spinMinus_eq_image_spinWeight_odd.

The diagonal bivectors

noncomputable def TauCeti.SpinPolarizationData.diagonalBivector {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} (b : Module.Basis ι K ↥P.W) [Invertible 2] (i : ι) : CliffordAlgebra Q

The i-th diagonal bivector of a polarization with a chosen basis of its isotropic summand: the Clifford bivector of the i-th basis vector and its dual.

Equations

• P.diagonalBivector b i = CliffordAlgebra.bivector Q ↑(b i) ↑(P.dualVector b i)

theorem TauCeti.SpinPolarizationData.diagonalBivector_def {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} (b : Module.Basis ι K ↥P.W) [Invertible 2] (i : ι) : P.diagonalBivector b i = CliffordAlgebra.bivector Q ↑(b i) ↑(P.dualVector b i)

theorem TauCeti.SpinPolarizationData.diagonalBivector_mem_quadraticLieSubalgebra {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} (b : Module.Basis ι K ↥P.W) [Invertible 2] (i : ι) : P.diagonalBivector b i ∈ CliffordAlgebra.quadraticLieSubalgebra Q

The diagonal bivectors are quadratic elements of the Clifford algebra, so they lie in the Lie subalgebra that realizes 𝔰𝔬(V, Q).

theorem TauCeti.SpinPolarizationData.lie_diagonalBivector_diagonalBivector {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (i j : ι) : ⁅P.diagonalBivector b i, P.diagonalBivector b j⁆ = 0

The diagonal bivectors commute. Of the four polar values entering the bracket of two Clifford bivectors only the two Kronecker pairings survive, and off the diagonal they vanish too; on the diagonal the two surviving contributions cancel.

The diagonal action on the exterior basis

theorem TauCeti.SpinPolarizationData.wedge_contract_dualVector_basis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) (i : ι) (s : Finset ι) : (P.wedge (b i)) ((P.contract (P.dualVector b i)) (b.ExteriorAlgebra s)) = if i ∈ s then b.ExteriorAlgebra s else 0

Creation after annihilation at the same index is the occupation projection: it fixes the exterior basis vectors containing that index and kills the others.

theorem TauCeti.SpinPolarizationData.contract_dualVector_wedge_basis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) (i : ι) (s : Finset ι) : (P.contract (P.dualVector b i)) ((P.wedge (b i)) (b.ExteriorAlgebra s)) = b.ExteriorAlgebra s - if i ∈ s then b.ExteriorAlgebra s else 0

Annihilation after creation at the same index is the complementary vacancy projection, by the creation–annihilation anticommutator and the Kronecker pairing.

@[simp]

theorem TauCeti.SpinPolarizationData.spinAction_diagonalBivector_basis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (i : ι) (s : Finset ι) : ((spinAction Q P) (P.diagonalBivector b i)) (b.ExteriorAlgebra s) = spinWeight K s i • b.ExteriorAlgebra s

The diagonal bivectors act diagonally on the exterior basis of the spinor module: the i-th one multiplies the basis vector indexed by s by ⅟2 when i ∈ s and by -⅟2 otherwise, so that basis vector is a weight vector of weight TauCeti.spinWeight K s.

theorem TauCeti.SpinPolarizationData.spinAction_two_smul_diagonalBivector_basis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (i : ι) (s : Finset ι) : ((spinAction Q P) (2 • P.diagonalBivector b i)) (b.ExteriorAlgebra s) = (if i ∈ s then 1 else -1) • b.ExteriorAlgebra s

Twice a diagonal bivector acts on the exterior basis by ±1, according to whether its coordinate is occupied: the spin weights are half-integral, so their doubles are units. This is the combination realized by the short coroot of an odd orthogonal Lie algebra.

theorem TauCeti.SpinPolarizationData.spinAction_diagonalBivector_sub_diagonalBivector_basis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (i j : ι) (s : Finset ι) : ((spinAction Q P) (P.diagonalBivector b i - P.diagonalBivector b j)) (b.ExteriorAlgebra s) = (spinWeight K s i - spinWeight K s j) • b.ExteriorAlgebra s

A difference of two diagonal bivectors acts on the exterior basis by the difference of the two spin weights, which is 0 or ±1. This is the combination realized by the long coroot of an orthogonal Lie algebra.

The weight-space decomposition

noncomputable def TauCeti.spinWeightSpace {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {ι : Type w} (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (b : Module.Basis ι K ↥P.W) (χ : ι → K) : Submodule K (ExteriorAlgebra K ↥P.W)

The weight space of the spinor module at a tuple χ of prescribed eigenvalues: the simultaneous eigenspace of the operators H i, the i-th one acting with eigenvalue χ i.

Equations

• TauCeti.spinWeightSpace Q P b χ = ⨅ (i : ι), ((TauCeti.spinAction Q P) (P.diagonalBivector b i)).eigenspace (χ i)

theorem TauCeti.spinWeightSpace_def {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} (b : Module.Basis ι K ↥P.W) (χ : ι → K) : spinWeightSpace Q P b χ = ⨅ (i : ι), ((spinAction Q P) (P.diagonalBivector b i)).eigenspace (χ i)

@[simp]

theorem TauCeti.mem_spinWeightSpace_iff {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} (b : Module.Basis ι K ↥P.W) {χ : ι → K} {x : ExteriorAlgebra K ↥P.W} : x ∈ spinWeightSpace Q P b χ ↔ ∀ (i : ι), ((spinAction Q P) (P.diagonalBivector b i)) x = χ i • x

Membership in a weight space, unfolded: a spinor lies in it exactly when every H i scales it by the prescribed eigenvalue χ i.

theorem TauCeti.basis_mem_spinWeightSpace {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) (s : Finset ι) : b.ExteriorAlgebra s ∈ spinWeightSpace Q P b (spinWeight K s)

The exterior basis vector indexed by s lies in the weight space at spinWeight K s.

theorem TauCeti.repr_spinAction_diagonalBivector {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) (i : ι) (t : Finset ι) (x : ExteriorAlgebra K ↥P.W) : (b.ExteriorAlgebra.repr (((spinAction Q P) (P.diagonalBivector b i)) x)) t = spinWeight K t i * (b.ExteriorAlgebra.repr x) t

The diagonal bivectors are diagonal in the exterior basis, read on coordinates: applying H i scales the t-th coordinate of any spinor by the i-th entry of the weight of t.

@[simp]

theorem TauCeti.spinWeightSpace_spinWeight {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) (s : Finset ι) : spinWeightSpace Q P b (spinWeight K s) = K ∙ b.ExteriorAlgebra s

Each weight space of the spinor module is a line, spanned by the exterior basis vector carrying that weight. Distinct sign vectors differ somewhere by a unit, which is what forces every other coordinate of a weight vector to vanish.

theorem TauCeti.spinWeightSpace_eq_bot_of_notMem_range {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [NoZeroDivisors K] {χ : ι → K} (hχ : χ ∉ Set.range (spinWeight K)) : spinWeightSpace Q P b χ = ⊥

No tuple of eigenvalues other than a sign vector occurs in the spinor module, over a ring without zero divisors.

@[simp]

theorem TauCeti.spinWeightSpace_ne_bot_iff {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Nontrivial K] [NoZeroDivisors K] {χ : ι → K} : spinWeightSpace Q P b χ ≠ ⊥ ↔ χ ∈ Set.range (spinWeight K)

The weights of the spinor module are exactly the sign vectors: a tuple of eigenvalues has a nonzero simultaneous eigenspace precisely when it is one of the TauCeti.spinWeight K s.

theorem TauCeti.iSup_spinWeightSpace_eq_top {K : Type u} [CommRing K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [LinearOrder ι] (b : Module.Basis ι K ↥P.W) : ⨆ (s : Finset ι), spinWeightSpace Q P b (spinWeight K s) = ⊤

The weight spaces exhaust the spinor module: the lines carrying the sign vectors span S = ⋀·W.