Symmetry of the weight multiplicities of an sl₂-module

Let (h, e, f) be an sl₂ triple acting on a finite-dimensional module over a field of characteristic zero. This file proves that the μ- and -μ-eigenspaces of the Cartan element h have the same dimension. Characteristic zero is essential: the argument runs along the integer ladders of the irreducible summands. The statement is made for an arbitrary triple in an arbitrary ambient Lie algebra; only its generated subalgebra acts in the argument.

The result is the rank-one symmetry needed for Weyl invariance of weight multiplicities. For a root α, restriction to its sl₂ triple identifies the reflection of a weight λ with the opposite weight on the corresponding α-string. Applying the theorem below to every such string gives the direct rank-one proof required by Layer 2 of the highest-weight roadmap, independently of Weyl's complete reducibility theorem.

The construction uses Ado.exists_isInternal_isIrreducible to decompose the module under the generated sl₂. On each irreducible summand, Ado.basisOfHasPrimitiveVectorWith is the ladder basis of weights n, n - 2, …, -n. Mathlib's DirectSum.IsInternal.collectedBasis joins these into a basis of the ambient module. Reversing every ladder gives a linear involution that anticommutes with h, hence restricts to an equivalence between the two eigenspaces. That construction needs an algebraically closed field; over a general field of characteristic zero the result follows by base change to the algebraic closure, which leaves both eigenspace dimensions unchanged.

Main result

• Ado.finrank_eigenspace_toEnd_neg: over a field of characteristic zero, the Cartan eigenspaces at μ and -μ have equal dimension.

References

This is the rank-one input to the "Weyl-invariance of multiplicities, directly from sl₂" target in Layer 2 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §13.2.

theorem Ado.finrank_eigenspace_toEnd_neg {K : Type u_1} [Field K] [CharZero K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {h e f : L} (t : IsSl2Triple h e f) (μ : K) : Module.finrank K ↥(((LieModule.toEnd K L M) h).eigenspace μ) = Module.finrank K ↥(((LieModule.toEnd K L M) h).eigenspace (-μ))

The weight multiplicities of a finite-dimensional sl₂-module are symmetric, over a field of characteristic zero. For the Cartan element h of any sl₂ triple, the eigenspaces of weights μ and -μ have the same dimension.

Only the Lie subalgebra generated by the triple is used. Thus the result applies directly to the triple attached to a root inside a larger semisimple Lie algebra, which is the rank-one input for Weyl invariance of the ambient module's weight multiplicities.