Invariant subspaces and intertwiners for the spinor and half-spin actions

The Fock model makes the exterior algebra S = ⋀·W of the isotropic summand of a polarization a module over CliffordAlgebra Q (TauCeti.spinAction), and that action is onto the full endomorphism algebra as soon as W is finite free (TauCeti.spinAction_surjective). A module on which every endomorphism is realized has no proper nonzero submodule at all, so the spinor module is simple, in every dimension and without any nondegeneracy hypothesis: this is TauCeti.exists_spinAction_eq, that a nonzero spinor is carried to every other one, and TauCeti.eq_bot_or_eq_top_of_map_spinAction_le, its lattice form.

That is not yet the irreducibility the spin representation is named for, because in even dimension S visibly splits, into the two half-spin summands S⁺ and S⁻ of TauCeti.spinPlus and TauCeti.spinMinus. The splitting is invariant not under the whole Clifford algebra but under its even subalgebra, and the theorem the splitting deserves is that the even subalgebra sees exactly those two pieces and nothing finer:

TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd : even Q ≃ₐ[K] Module.End K S⁺ × Module.End K S⁻.

The proof of that structure theorem does not count dimensions a second time. Surjectivity onto the product comes from the full structure theorem TauCeti.spinAction_bijective together with the parity bookkeeping of TauCeti/RepresentationTheory/Spin/HalfSpin/Basic.lean. This file records its representation-theoretic consequences: each half-spin summand has no proper nonzero invariant subspace because its factor is a full endomorphism algebra, and the two even-Clifford actions are inequivalent (TauCeti.not_exists_equiv_intertwines_spinPlusAction_spinMinusAction) because the element of even Q acting as the identity on S⁺ and as zero on S⁻ kills any map that intertwines them.

The invariant-subspace conclusions for the even Clifford algebra are stated in lattice form, as "an invariant subspace is ⊥ or everything", rather than as IsSimpleModule: S⁺ and S⁻ carry no Module (even Q) instance, and manufacturing one would mean a type synonym for a statement that reads no better through it. Over a separably closed field, the Spin group linearly spans the even Clifford algebra when the quadratic form is nondegenerate and the characteristic is not two. The same dichotomies therefore prove that the even half-spin subrepresentation is irreducible, that the odd half is irreducible when P.W ≠ ⊥, and that the two are inequivalent.

The actions themselves — TauCeti.spinPlusAction, TauCeti.spinMinusAction and their pair TauCeti.evenSpinActionProd — are defined in TauCeti/RepresentationTheory/Spin/HalfSpin/Basic.lean, beside the bundling of the same two summands as subrepresentations of spinRep that the same invariance gives; this file only proves theorems about them.

The hypothesis P.line = ⊥ is the even-dimensional case, and it is exactly what makes the parity splitting a splitting of modules at all; TauCeti.SpinPolarizationData.even_finrank_of_line_eq_bot turns it into the evenness the structure theorem is stated with, so no separate parity hypothesis is carried. The lattice dichotomy for S⁻ needs no further hypothesis, since it also holds vacuously when S⁻ = 0. To conclude that S⁻ is simple, combine it with TauCeti.nontrivial_spinMinus, whose hypothesis W ≠ ⊥ rules out only the zero-dimensional quadratic space: there S = K is entirely even and S⁻ is zero. S⁺ always contains the scalars, so it needs no such hypothesis, and neither does the inequivalence.

The odd-dimensional case is the opposite of all this, and the last section records it. There the even subalgebra is a single block rather than a product, so the Fock action already carries it onto all of Module.End K S (TauCeti.evenSpinAction_surjective), and the whole spinor module — not a half of it — is the irreducible object: TauCeti.spinRep_isIrreducible_of_odd. As soon as P.W ≠ ⊥, exterior parity still splits S as a vector space but no longer as a representation, which TauCeti.not_forall_map_spinRep_spinPlus_le and TauCeti.not_forall_map_spinRep_spinMinus_le record: neither half is ⊥ or everything, so irreducibility alone forbids either from being invariant. The P.line = ⊥ carried by every statement of the even-dimensional half is precisely what fails. Dimension one is the exception: there W = ⊥ and S = K is entirely even, so S⁺ = S and S⁻ = 0 are both invariant, for want of anything to split.

The two parities are separated by exactly one hypothesis, the surjectivity of TauCeti.evenSpinAction, and TauCeti.isIrreducible_spinRep_of_span_of_surjective is stated against it rather than against a dimension, so the dichotomy is visible in the statement. It fails in even dimension except for the zero-dimensional quadratic space, where S = K is one-dimensional and there is no room for it to fail.

What is not proved here is the odd-dimensional splitting of CliffordAlgebra Q into its two central summands, for which the results here are the even-dimensional half; it is CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one.

Main results

• TauCeti.exists_spinAction_eq and TauCeti.eq_bot_or_eq_top_of_map_spinAction_le: the spinor module is a simple Clifford module.
• TauCeti.mem_even_of_map_spinPlus_le_of_map_spinMinus_le: a Clifford element whose action preserves both half-spin summands is even.
• TauCeti.eq_bot_or_eq_top_of_map_spinPlusAction_le and TauCeti.eq_bot_or_eq_top_of_map_spinMinusAction_le: the two half-spin summands have no proper nonzero invariant subspace. Together with TauCeti.nontrivial_spinPlus and TauCeti.nontrivial_spinMinus, respectively, these say that the summands are simple.
• TauCeti.eq_zero_of_intertwines_spinPlusAction_spinMinusAction and TauCeti.eq_zero_of_intertwines_spinMinusAction_spinPlusAction: there is no nonzero map either way intertwining the two actions, and hence TauCeti.not_exists_equiv_intertwines_spinPlusAction_spinMinusAction: the half-spin summands are inequivalent.
• TauCeti.isIrreducible_spinPlusSubrep_of_span and TauCeti.isIrreducible_spinMinusSubrep_of_span: the two half-spin group representations are irreducible when the Spin group spans the even Clifford algebra, with P.W ≠ ⊥ required for the odd half. The _of_isSquare and suffix-free versions give progressively stronger sufficient hypotheses.
• TauCeti.isEmpty_equiv_spinPlusSubrep_spinMinusSubrep_of_span: the two half-spin group representations are inequivalent under the same spanning hypothesis, with analogous corollaries.
• TauCeti.isIrreducible_spinRep_of_span_of_surjective: the spin representation is irreducible once the Spin group spans the even subalgebra and that subalgebra exhausts the endomorphisms of the spinor module.
• TauCeti.isIrreducible_spinRep_of_isSquare and TauCeti.spinRep_isIrreducible_of_odd: the spin representation is irreducible in odd dimension, the type Bₗ half of Layer 4, under the square normalization and over a separably closed field respectively.
• TauCeti.not_forall_map_spinRep_spinPlus_le_of_isIrreducible and TauCeti.not_forall_map_spinRep_spinMinus_le_of_isIrreducible: an irreducible spinor module does not split along exterior parity, provided P.W ≠ ⊥, which rules out only dimension one; TauCeti.not_forall_map_spinRep_spinPlus_le and TauCeti.not_forall_map_spinRep_spinMinus_le are their odd-dimensional specializations.

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 is the endomorphism algebra of ⋀·W, its even subalgebra is the product of the endomorphism algebras of the two halves, and the two half-spin modules are irreducible and inequivalent; §20.2 for the odd-dimensional spin representation, which does not split.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry, Princeton University Press (1989), Chapter I, §5: the complex spinor representations and their irreducibility in both parities.
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.
• Spin-representations roadmap, Layers 1 and 4, "the structure theorem" and "the spin and half-spin representations".

The spinor module is a simple Clifford module

Nothing here needs an even dimension, a nondegenerate form, or an invertible 2: the Fock action is onto Module.End K S for every polarization whose isotropic summand is finite-dimensional, and a vector space is a simple module over its own endomorphism ring.

theorem TauCeti.exists_spinAction_eq {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K ↥P.W] {s : ExteriorAlgebra K ↥P.W} (hs : s ≠ 0) (t : ExteriorAlgebra K ↥P.W) : ∃ (x : CliffordAlgebra Q), ((spinAction Q P) x) s = t

A nonzero spinor generates the spinor module: some Clifford element carries it to any prescribed spinor. The Fock action realizes every endomorphism of S = ⋀·W, and a vector space is a simple module over its endomorphism ring.

theorem TauCeti.eq_bot_or_eq_top_of_map_spinAction_le {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K ↥P.W] (N : Submodule K (ExteriorAlgebra K ↥P.W)) (hN : ∀ (x : CliffordAlgebra Q), Submodule.map ((spinAction Q P) x) N ≤ N) : N = ⊥ ∨ N = ⊤

The invariant-subspace dichotomy for the spinor module: a submodule of S = ⋀·W invariant under every Clifford element is ⊥ or the whole of S. The spinor module is nonzero, so this is its simplicity statement for the Clifford action.

Consequences of the even structure theorem

Invariant-subspace dichotomies and inequivalence of the two half-spin actions

theorem TauCeti.eq_bot_or_eq_top_of_map_spinPlusAction_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 = ⊥) (N : Submodule K ↥(spinPlus Q P)) (hN : ∀ (x : ↥(CliffordAlgebra.even Q)), Submodule.map ((spinPlusAction Q P hline) x) N ≤ N) : N = ⊥ ∨ N = ⊤

The invariant-subspace dichotomy for the even half-spin summand: every subspace of S⁺ invariant under the even Clifford subalgebra is ⊥ or all of S⁺. Combine this with TauCeti.nontrivial_spinPlus to obtain simplicity.

theorem TauCeti.eq_bot_or_eq_top_of_map_spinMinusAction_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 = ⊥) (N : Submodule K ↥(spinMinus Q P)) (hN : ∀ (x : ↥(CliffordAlgebra.even Q)), Submodule.map ((spinMinusAction Q P hline) x) N ≤ N) : N = ⊥ ∨ N = ⊤

The invariant-subspace dichotomy for the odd half-spin summand: every subspace of S⁻ invariant under the even Clifford subalgebra is ⊥ or all of S⁻. This remains true when S⁻ is zero; combine it with TauCeti.nontrivial_spinMinus to obtain simplicity when P.W ≠ ⊥.

theorem TauCeti.eq_zero_of_intertwines_spinPlusAction_spinMinusAction {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 = ⊥) (φ : ↥(spinPlus Q P) →ₗ[K] ↥(spinMinus Q P)) (hφ : ∀ (x : ↥(CliffordAlgebra.even Q)) (s : ↥(spinPlus Q P)), φ (((spinPlusAction Q P hline) x) s) = ((spinMinusAction Q P hline) x) (φ s)) : φ = 0

A map intertwining the two half-spin actions is zero. The even subalgebra contains an element acting as the identity on S⁺ and as zero on S⁻, and an intertwiner turns the first statement into the second.

theorem TauCeti.eq_zero_of_intertwines_spinMinusAction_spinPlusAction {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 = ⊥) (φ : ↥(spinMinus Q P) →ₗ[K] ↥(spinPlus Q P)) (hφ : ∀ (x : ↥(CliffordAlgebra.even Q)) (s : ↥(spinMinus Q P)), φ (((spinMinusAction Q P hline) x) s) = ((spinPlusAction Q P hline) x) (φ s)) : φ = 0

A map intertwining the odd and even half-spin actions is zero.

theorem TauCeti.not_exists_equiv_intertwines_spinPlusAction_spinMinusAction {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 = ⊥) : ¬∃ (e : ↥(spinPlus Q P) ≃ₗ[K] ↥(spinMinus Q P)), ∀ (x : ↥(CliffordAlgebra.even Q)) (s : ↥(spinPlus Q P)), e (((spinPlusAction Q P hline) x) s) = ((spinMinusAction Q P hline) x) (e s)

The two half-spin summands are inequivalent. There is no linear equivalence intertwining the two actions of the even Clifford subalgebra.

Irreducibility of the half-spin group representations

theorem TauCeti.isIrreducible_spinPlusSubrep_of_span {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) (hspan : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (CliffordAlgebra.even Q)) (hline : P.line = ⊥) : (spinPlusSubrep P hline).toRepresentation.IsIrreducible

The even half-spin representation of the Spin group is irreducible when the Spin group linearly spans the even Clifford algebra.

theorem TauCeti.isIrreducible_spinMinusSubrep_of_span {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) (hspan : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (CliffordAlgebra.even Q)) (hline : P.line = ⊥) (hW : P.W ≠ ⊥) : (spinMinusSubrep P hline).toRepresentation.IsIrreducible

The odd half-spin representation of the Spin group is irreducible when the odd summand is nonzero and the Spin group linearly spans the even Clifford algebra.

theorem TauCeti.isEmpty_equiv_spinPlusSubrep_spinMinusSubrep_of_span {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) (hspan : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (CliffordAlgebra.even Q)) (hline : P.line = ⊥) : IsEmpty ((spinPlusSubrep P hline).toRepresentation.Equiv (spinMinusSubrep P hline).toRepresentation)

The two half-spin representations of the Spin group are inequivalent when the Spin group linearly spans the even Clifford algebra.

theorem TauCeti.isIrreducible_spinPlusSubrep_of_isSquare {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) (hsq : ∀ (v w : V), Q v ≠ 0 → Q w ≠ 0 → IsSquare ((Q v)⁻¹ * (Q w)⁻¹)) (hline : P.line = ⊥) : (spinPlusSubrep P hline).toRepresentation.IsIrreducible

The even half-spin representation of the Spin group is irreducible when anisotropic pairs admit the square normalization needed to span the even Clifford algebra.

theorem TauCeti.isIrreducible_spinMinusSubrep_of_isSquare {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) (hsq : ∀ (v w : V), Q v ≠ 0 → Q w ≠ 0 → IsSquare ((Q v)⁻¹ * (Q w)⁻¹)) (hline : P.line = ⊥) (hW : P.W ≠ ⊥) : (spinMinusSubrep P hline).toRepresentation.IsIrreducible

The odd half-spin representation of the Spin group is irreducible when the odd summand is nonzero and anisotropic pairs admit the required square normalization.

theorem TauCeti.isEmpty_equiv_spinPlusSubrep_spinMinusSubrep_of_isSquare {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) (hsq : ∀ (v w : V), Q v ≠ 0 → Q w ≠ 0 → IsSquare ((Q v)⁻¹ * (Q w)⁻¹)) (hline : P.line = ⊥) : IsEmpty ((spinPlusSubrep P hline).toRepresentation.Equiv (spinMinusSubrep P hline).toRepresentation)

The two half-spin representations of the Spin group are inequivalent when anisotropic pairs admit the square normalization needed to span the even Clifford algebra.

theorem TauCeti.isIrreducible_spinPlusSubrep {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) [IsSepClosed K] (hline : P.line = ⊥) : (spinPlusSubrep P hline).toRepresentation.IsIrreducible

The even half-spin representation of the Spin group is irreducible over a separably closed field for polarization data without a line remainder.

theorem TauCeti.isIrreducible_spinMinusSubrep {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) [IsSepClosed K] (hline : P.line = ⊥) (hW : P.W ≠ ⊥) : (spinMinusSubrep P hline).toRepresentation.IsIrreducible

The odd half-spin representation of the Spin group is irreducible over a separably closed field when the odd summand is nonzero.

theorem TauCeti.isEmpty_equiv_spinPlusSubrep_spinMinusSubrep {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) [IsSepClosed K] (hline : P.line = ⊥) : IsEmpty ((spinPlusSubrep P hline).toRepresentation.Equiv (spinMinusSubrep P hline).toRepresentation)

The two half-spin representations of the Spin group are inequivalent over a separably closed field.

Irreducibility of the spin representation in odd dimension

theorem TauCeti.isIrreducible_spinRep_of_span_of_surjective {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hspan : Submodule.span K ↑(spinGroup Q) = Subalgebra.toSubmodule (CliffordAlgebra.even Q)) (hsurj : Function.Surjective ⇑(evenSpinAction Q P)) : (spinRep Q P).IsIrreducible

The whole spin representation is irreducible as soon as the Spin group linearly spans the even Clifford subalgebra and that subalgebra already exhausts the endomorphisms of the spinor module.

The second hypothesis is exactly what separates the two parities of finrank K V. In positive even dimension it fails — the even subalgebra is the product of the two half-spin endomorphism algebras, by TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd, and S visibly splits — and in odd dimension it holds, by TauCeti.evenSpinAction_surjective. Dimension zero is the exception on the even side: there W = ⊥, the odd block is zero, S = K is one-dimensional and the even subalgebra is already all of Module.End K S.

theorem TauCeti.not_forall_map_spinRep_spinPlus_le_of_isIrreducible {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hirr : (spinRep Q P).IsIrreducible) (hW : P.W ≠ ⊥) : ¬∀ (g : ↥(spinGroup Q)), Submodule.map ((spinRep Q P) g) (spinPlus Q P) ≤ spinPlus Q P

An irreducible spinor module does not split along exterior parity. The even part S⁺ is not invariant under the Spin group, so it is not a subrepresentation of spinRep.

Nothing about the anisotropic remainder is computed: the proof is by irreducibility, S⁺ being neither ⊥ (it contains the scalars) nor everything (it misses the nonzero S⁻). The hypothesis P.W ≠ ⊥ is what excludes finrank K V = 1, where S = K is entirely even, S⁺ = S is trivially invariant and there is nothing to split. In even dimension the same subspace is invariant, by TauCeti.spinPlus_invariant, and spinRep is correspondingly reducible.

theorem TauCeti.not_forall_map_spinRep_spinMinus_le_of_isIrreducible {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hirr : (spinRep Q P).IsIrreducible) (hW : P.W ≠ ⊥) : ¬∀ (g : ↥(spinGroup Q)), Submodule.map ((spinRep Q P) g) (spinMinus Q P) ≤ spinMinus Q P

The odd half of an irreducible spinor module is not invariant either. The companion of TauCeti.not_forall_map_spinRep_spinPlus_le_of_isIrreducible for the other parity: S⁻ is nonzero when P.W ≠ ⊥ and is not everything, S⁺ containing the scalars, so irreducibility forbids it from being a subrepresentation of spinRep.

theorem TauCeti.isIrreducible_spinRep_of_isSquare {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [NeZero 2] [FiniteDimensional K V] (hsq : ∀ (v w : V), Q v ≠ 0 → Q w ≠ 0 → IsSquare ((Q v)⁻¹ * (Q w)⁻¹)) (hodd : Odd (Module.finrank K V)) : (spinRep Q P).IsIrreducible

The spin representation is irreducible in odd dimension when anisotropic pairs admit the square normalization needed to span the even Clifford algebra.

This is the generality of the even-dimensional TauCeti.isIrreducible_spinPlusSubrep_of_isSquare: no separably closed field, and no nondegeneracy hypothesis, the polarization data already carrying it by TauCeti.SpinPolarizationData.nondegenerate. The square normalization is only what lifts a product of two reflections to the Spin group, and it is the sole remaining hypothesis of this argument.

theorem TauCeti.spinRep_isIrreducible_of_odd {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [NeZero 2] [FiniteDimensional K V] [IsSepClosed K] (l : ℕ) (hV : Module.finrank K V = 2 * l + 1) : (spinRep Q P).IsIrreducible

The spin representation is irreducible in odd dimension. For a polarized quadratic space of dimension 2 * l + 1 over a separably closed field of characteristic not two, the Spin group acts irreducibly on the whole spinor module S = ⋀·W.

This is the type Bₗ half of the Layer-4 irreducibility statement, in the shape the roadmap pins. Nondegeneracy of Q is not assumed: the polarization data already carries it, by TauCeti.SpinPolarizationData.nondegenerate. Except in dimension one, where W = ⊥ and S = K is entirely even, the exterior parity splitting S = S⁺ ⊕ S⁻ is not a splitting of representations here: see TauCeti.not_forall_map_spinRep_spinPlus_le. The even-dimensional counterpart is the pair TauCeti.isIrreducible_spinPlusSubrep, TauCeti.isIrreducible_spinMinusSubrep, where S itself is reducible unless it is the zero-dimensional quadratic space.

theorem TauCeti.not_forall_map_spinRep_spinPlus_le {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [NeZero 2] [FiniteDimensional K V] [IsSepClosed K] (l : ℕ) (hV : Module.finrank K V = 2 * l + 1) (hW : P.W ≠ ⊥) : ¬∀ (g : ↥(spinGroup Q)), Submodule.map ((spinRep Q P) g) (spinPlus Q P) ≤ spinPlus Q P

In odd dimension the spinor module does not split along exterior parity. The separably closed specialization of TauCeti.not_forall_map_spinRep_spinPlus_le_of_isIrreducible, where TauCeti.spinRep_isIrreducible_of_odd supplies the irreducibility. Unlike in positive even dimension, S⁺ is not a subrepresentation of spinRep; the hypothesis P.line = ⊥ carried by TauCeti.spinPlus_invariant is what an odd-dimensional polarization cannot satisfy.

theorem TauCeti.not_forall_map_spinRep_spinMinus_le {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [NeZero 2] [FiniteDimensional K V] [IsSepClosed K] (l : ℕ) (hV : Module.finrank K V = 2 * l + 1) (hW : P.W ≠ ⊥) : ¬∀ (g : ↥(spinGroup Q)), Submodule.map ((spinRep Q P) g) (spinMinus Q P) ≤ spinMinus Q P

In odd dimension the odd half of the spinor module is not invariant either. The companion of TauCeti.not_forall_map_spinRep_spinPlus_le for the other parity, the separably closed specialization of TauCeti.not_forall_map_spinRep_spinMinus_le_of_isIrreducible.