Documentation

TauCeti.RepresentationTheory.Spin.HalfSpin.Weight

The weights of the half-spin summands #

TauCeti/RepresentationTheory/Spin/Weight.lean diagonalizes the spinor module S = ⋀·W of a polarization under the commuting diagonal bivectors H i: the weight spaces are the lines spanned by the exterior basis vectors, the weight of the vector indexed by a finite set s of coordinates being the sign vector spinWeight K s = ½(±1, …, ±1) whose + signs are the elements of s. TauCeti/RepresentationTheory/Spin/HalfSpin/Basic.lean splits the same module along exterior parity, as S⁺ ⊕ S⁻.

This file matches the two decompositions. Each is indexed by the exterior basis, so they are compatible in the strongest sense: every weight line lies in one of the two half-spin summands, and which one is decided by the parity of the number of + signs of its weight. So the weights of S⁺ are the sign vectors with an even number of + signs, those of S⁻ the ones with an odd number, and S⁺ and S⁻ are the sums of the corresponding weight lines.

The count that comes with this is the one a half-spin representation should have. On l coordinates there are 2 ^ l sign vectors (TauCeti.ncard_range_spinWeight), and for l > 0 parity splits them evenly, so each summand carries 2 ^ (l - 1) weights. On no coordinates at all the split is uneven: the one sign vector is the empty one, which is even, so S⁺ carries that single weight and S⁻ carries none — which is why TauCeti.ncard_setOf_spinWeightSpace_ne_bot_and_le_spinMinus asks the coordinates to be nonempty and its S⁺ counterpart does not. Over a field, and for a polarization whose W is finite-dimensional and nonzero, 2 ^ (l - 1) is also the dimension of each summand, computed independently in TauCeti/RepresentationTheory/Spin/Dimension.lean by a Clifford-algebraic argument (TauCeti.finrank_spinPlus and TauCeti.finrank_spinMinus, both of which exclude W = ⊥, the same degenerate case).

Nothing here needs a field, a nondegeneracy hypothesis, a finite dimension, or a polarization without a line summand: the parity grading of ⋀·W and the diagonalization are both available over the commutative ring the polarization data lives over. The parity statements of the first section hold over any commutative ring, nontriviality being needed only where a parity is read off a basis vector, that vector having to be nonzero for its parity to be well defined. The weight-space statements inherit from TauCeti/RepresentationTheory/Spin/Weight.lean the standing hypothesis that 2 be invertible — without it the sign vector TauCeti.spinWeight is not even defined — and that is the only extra hypothesis the inclusions and the identification of the two summands carry; the exact descriptions of the weight sets of S⁺ and S⁻, and the two counts of weights read off them, ask in addition that K have no zero divisors, since deciding which weight spaces are nonzero does.

As in TauCeti/RepresentationTheory/Spin/Weight.lean, "weight" means a tuple of simultaneous eigenvalues for the family H, no Cartan subalgebra being exhibited; and no weight is called highest, since no ordering of the coordinates is used to single out a Borel. What the parity statements do supply for the type-Dₗ fork is the parity flip between the two candidate highest-weight vectors of TauCeti/RepresentationTheory/Spin/Polarization/TypeD/ForkWeights.lean: by TauCeti.basis_mem_spinPlus_iff_basis_erase_mem_spinMinus, specialized to ι = Fin n at s = Finset.univ and i the final coordinate ⟨n - 1, _⟩ — the coordinate that ForkWeights.lean erases — the basis vector with every coordinate occupied lies in S⁺ exactly when the one obtained from it by erasing that final coordinate lies in S⁻. For an arbitrary index type the theorem erases an arbitrary occupied coordinate, that generality having no fork reading. That equivalence between two memberships is all it says; which summand each of the two vectors actually lies in is read off TauCeti.basis_mem_spinPlus_iff and TauCeti.basis_mem_spinMinus_iff, from the parity of the number of coordinates.

Main results #

References #

source
theorem TauCeti.basis_mem_spinPlus_iff {K : Type u} [CommRing K] [Nontrivial 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) (s : Finset ι) :
b.ExteriorAlgebra s ∈ spinPlus Q P ↔ Even s.card

An exterior basis vector lies in S⁺ exactly when it has an even number of coordinates. The statement itself does not need 2 to be invertible. Where it is — the hypothesis under which the sign vector TauCeti.spinWeight is defined at all — the + signs of the weight of this vector are by definition its coordinates, so the condition also says that its weight has an even number of + signs; read on the weight line that is TauCeti.spinWeightSpace_le_spinPlus_iff.

source
theorem TauCeti.basis_mem_spinMinus_iff {K : Type u} [CommRing K] [Nontrivial 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) (s : Finset ι) :
b.ExteriorAlgebra s ∈ spinMinus Q P ↔ Odd s.card

An exterior basis vector lies in S⁻ exactly when it has an odd number of coordinates. The statement itself does not need 2 to be invertible. Where it is — the hypothesis under which the sign vector TauCeti.spinWeight is defined at all — the + signs of the weight of this vector are by definition its coordinates, so the condition also says that its weight has an odd number of + signs; read on the weight line that is TauCeti.spinWeightSpace_le_spinMinus_iff.

source
theorem TauCeti.basis_mem_spinPlus_iff_basis_erase_mem_spinMinus {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) {s : Finset ι} {i : ι} (hi : i ∈ s) :
b.ExteriorAlgebra s ∈ spinPlus Q P ↔ b.ExteriorAlgebra (s.erase i) ∈ spinMinus Q P

Erasing an occupied coordinate flips the summand. A basis vector lies in S⁺ exactly when the vector obtained from it by erasing one of its coordinates lies in S⁻, erasing a coordinate changing the parity of the number of coordinates. This is the equivalence of the two memberships only: which of the two summands each vector actually lies in depends on the parity of the number of coordinates, and is TauCeti.basis_mem_spinPlus_iff together with TauCeti.basis_mem_spinMinus_iff. Specialized to ι = Fin n at s = Finset.univ and i the final coordinate ⟨n - 1, _⟩, the two vectors are the ones that TauCeti/RepresentationTheory/Spin/Polarization/TypeD/ForkWeights.lean shows to be annihilated by every positive simple generator, with the type-Dₗ fork fundamental weights; at any other i, or over any other index type, the statement is not about that fork.

source
theorem TauCeti.basis_mem_spinMinus_iff_basis_erase_mem_spinPlus {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) {s : Finset ι} {i : ι} (hi : i ∈ s) :
b.ExteriorAlgebra s ∈ spinMinus Q P ↔ b.ExteriorAlgebra (s.erase i) ∈ spinPlus Q P

Erasing an occupied coordinate flips the summand, the other half of TauCeti.basis_mem_spinPlus_iff_basis_erase_mem_spinMinus: a basis vector lies in S⁻ exactly when the vector obtained from it by erasing one of its coordinates lies in S⁺.

source
theorem TauCeti.spinWeightSpace_le_spinPlus_iff {K : Type u} [CommRing K] [Invertible 2] [Nontrivial 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) (s : Finset ι) :
spinWeightSpace Q P b (spinWeight K s) ≤ spinPlus Q P ↔ Even s.card

A weight line lies in S⁺ exactly when its sign vector has an even number of + signs. The weight space is the line spanned by an exterior basis vector, so this is TauCeti.basis_mem_spinPlus_iff read on that line.

source
theorem TauCeti.spinWeightSpace_le_spinMinus_iff {K : Type u} [CommRing K] [Invertible 2] [Nontrivial 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) (s : Finset ι) :
spinWeightSpace Q P b (spinWeight K s) ≤ spinMinus Q P ↔ Odd s.card

A weight line lies in S⁻ exactly when its sign vector has an odd number of + signs.

source
theorem TauCeti.iSup_spinWeightSpace_even_le_spinPlus {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 ι), ⨆ (_ : Even s.card), spinWeightSpace Q P b (spinWeight K s) ≤ spinPlus Q P

The sum of the weight lines of even parity is contained in S⁺.

source
theorem TauCeti.iSup_spinWeightSpace_odd_le_spinMinus {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 ι), ⨆ (_ : Odd s.card), spinWeightSpace Q P b (spinWeight K s) ≤ spinMinus Q P

The sum of the weight lines of odd parity is contained in S⁻.

source
theorem TauCeti.iSup_spinWeightSpace_even_eq_spinPlus {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 ι), ⨆ (_ : Even s.card), spinWeightSpace Q P b (spinWeight K s) = spinPlus Q P

S⁺ is the sum of the weight lines of even parity.

source
theorem TauCeti.iSup_spinWeightSpace_odd_eq_spinMinus {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 ι), ⨆ (_ : Odd s.card), spinWeightSpace Q P b (spinWeight K s) = spinMinus Q P

S⁻ is the sum of the weight lines of odd parity, the other half of TauCeti.iSup_spinWeightSpace_even_eq_spinPlus.

source
theorem TauCeti.setOf_spinWeightSpace_ne_bot_and_le_spinPlus_eq_image_spinWeight_even {K : Type u} [CommRing K] [Invertible 2] [Nontrivial 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) [NoZeroDivisors K] :
{χ : ι → K | spinWeightSpace Q P b χ ≠ ⊥ ∧ spinWeightSpace Q P b χ ≤ spinPlus Q P} = spinWeight K '' {s : Finset ι | Even s.card}

The weights of S⁺ are exactly the sign vectors with an even number of + signs. A tuple of eigenvalues counts as a weight of S⁺ when its weight space is nonzero and contained in S⁺; the nonvanishing clause is what rules out the tuples that occur nowhere, whose weight space is ⊥ and so vacuously contained in both summands.

source
theorem TauCeti.setOf_spinWeightSpace_ne_bot_and_le_spinMinus_eq_image_spinWeight_odd {K : Type u} [CommRing K] [Invertible 2] [Nontrivial 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) [NoZeroDivisors K] :
{χ : ι → K | spinWeightSpace Q P b χ ≠ ⊥ ∧ spinWeightSpace Q P b χ ≤ spinMinus Q P} = spinWeight K '' {s : Finset ι | Odd s.card}

The weights of S⁻ are exactly the sign vectors with an odd number of + signs.

source
theorem TauCeti.ncard_setOf_spinWeightSpace_ne_bot_and_le_spinPlus {K : Type u} [CommRing K] [Invertible 2] [Nontrivial 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) [NoZeroDivisors K] [Finite ι] :
{χ : ι → K | spinWeightSpace Q P b χ ≠ ⊥ ∧ spinWeightSpace Q P b χ ≤ spinPlus Q P}.ncard = 2 ^ (Nat.card ι - 1)

S⁺ carries 2 ^ (l - 1) weights on l coordinates: for l > 0 half the 2 ^ l weights of the spinor module, the other half being those of S⁻ (TauCeti.ncard_setOf_spinWeightSpace_ne_bot_and_le_spinMinus); on no coordinates at all it is no half but the one weight the whole spinor module has, the empty sign vector being even, and 2 ^ (0 - 1) = 1 counts it. Over a field and on nonempty coordinates this is the dimension TauCeti.finrank_spinPlus of S⁺, as it must be, each weight space being a line.

source
theorem TauCeti.ncard_setOf_spinWeightSpace_ne_bot_and_le_spinMinus {K : Type u} [CommRing K] [Invertible 2] [Nontrivial 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) [NoZeroDivisors K] [Finite ι] [Nonempty ι] :
{χ : ι → K | spinWeightSpace Q P b χ ≠ ⊥ ∧ spinWeightSpace Q P b χ ≤ spinMinus Q P}.ncard = 2 ^ (Nat.card ι - 1)

S⁻ carries 2 ^ (l - 1) weights, matching TauCeti.finrank_spinMinus over a field. Unlike its S⁺ counterpart this asks the coordinates to be nonempty, there being no weight at all of odd parity on none.