Weyl invariance of the weight multiplicities of a module

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero, let H be a Cartan subalgebra and let M be a finite-dimensional L-module. The weight spaces of M are honest simultaneous eigenspaces of H (Ado.genWeightSpace_eq_weightSpace), so χ ↦ dim Mχ counts honest multiplicities. This file proves that this multiplicity function is invariant under the Weyl group of the root system of H; in particular the set of weights of M is stable under every reflection s_α.

The proof is the direct rank-one argument, not a corollary of Weyl's complete reducibility theorem. That matters for the order of the development: the highest-weight theory wants Weyl invariance of multiplicities before complete reducibility for L, whose usual proof consumes the weight theory, and routing this statement through complete reducibility would make the dependency circular. Only complete reducibility for sl₂ is used here, through Ado.finrank_eigenspace_toEnd_neg.

The argument, for a root α and a linear form χ, runs as follows.

• Cut the α-string through χ off at both ends: choose indices p and q beyond the two of interest, with M_{p α + χ} = M_{q α + χ} = 0, which is possible because a finite-dimensional module has only finitely many weights (LieModule.eventually_genWeightSpace_smul_add_eq_bot). Mathlib's LieModule.genWeightSpaceChain is then a module over the sl₂ triple (α^∨, eₐ, fₐ) attached to α: it is stable under H, and its two cut-off lemmas say exactly that it is stable under eₐ and fₐ.
• Inside the string the coroot α^∨ separates the weights: it acts on M_{k α + χ} by 2k + χ(α^∨), and these scalars are distinct, so each summand of the string is recovered from a single eigenspace of α^∨ (Ado.biSup_inf_eigenspace_eq_self).
• The sl₂ engine says the c- and (-c)-eigenspaces of the Cartan element have equal dimension on the string. Reading that back through the previous step turns it into the equality of the multiplicities at k α + χ and at (-k - χ(α^∨)) α + χ, whose k = 0 case is the reflection s_α χ = χ - χ(α^∨) • α.

Integrality of χ(α^∨) enters only to know that the reflected form lies on the string at all; when it fails, neither form is a weight and both multiplicities are zero, by Ado.genWeightSpaceOf_coroot_eq_bot_of_forall_ne_intCast.

Main results

• Ado.finrank_weightSpace_neg_sub_zsmul_add: the multiplicities along an α-string are symmetric about the midpoint of the reflection.
• Ado.finrank_weightSpace_sub_apply_coroot_smul: the reflection s_α preserves weight multiplicities, with no integrality hypothesis.
• Ado.weightSpace_sub_apply_coroot_smul_eq_bot_iff: consequently the set of weights of M is stable under the reflections.
• Ado.finrank_weightSpace_weylGroup_smul: Weyl invariance. The multiplicity function on the dual Module.Dual K H is invariant under the whole Weyl group of LieAlgebra.IsKilling.rootSystem H, and Ado.weightSpace_weylGroup_smul_eq_bot_iff records the resulting stability of the set of weights.

References

This is the "Weyl-invariance of multiplicities, directly from sl₂" item of Layer 2 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §21.2.

The α-string as a module over the sl₂ triple attached to α

Reflection symmetry of the multiplicities

theorem Ado.finrank_weightSpace_neg_sub_zsmul_add {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {α : LieModule.Weight K (↥H) L} {χ : ↥H → K} {n : ℤ} (hn : χ (LieAlgebra.IsKilling.coroot α) = ↑n) (k : ℤ) : Module.finrank K ↥(LieModule.weightSpace M ((-k - n) • ⇑α + χ)) = Module.finrank K ↥(LieModule.weightSpace M (k • ⇑α + χ))

Reflection symmetry of the weight multiplicities along a root string. Let α be a weight of L and let χ be a function on the Cartan subalgebra whose value on the coroot α^∨ is the integer n. Then along the whole α-string through χ, the multiplicities are symmetric about the midpoint of the reflection: the weight spaces at (-k - n) • α + χ and at k • α + χ have the same dimension.

For k = 0 this is the reflection s_α χ = χ - χ(α^∨) • α, which is Ado.finrank_weightSpace_sub_apply_coroot_smul below.

@[simp]

theorem Ado.finrank_weightSpace_sub_apply_coroot_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (α : LieModule.Weight K (↥H) L) (χ : ↥H → K) : Module.finrank K ↥(LieModule.weightSpace M (χ - χ (LieAlgebra.IsKilling.coroot α) • ⇑α)) = Module.finrank K ↥(LieModule.weightSpace M χ)

The reflection in a root preserves weight multiplicities. For a weight α of a Killing-semisimple Lie algebra and any function χ on the Cartan subalgebra, the weight spaces of a finite-dimensional module at χ and at its reflection s_α χ = χ - χ(α^∨) • α have the same dimension.

No integrality hypothesis is needed: if χ(α^∨) is not an integer then neither χ nor s_α χ is a weight of M, both weight spaces are trivial, and the statement is 0 = 0.

@[simp]

theorem Ado.weightSpace_sub_apply_coroot_smul_eq_bot_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (α : LieModule.Weight K (↥H) L) (χ : ↥H → K) : LieModule.weightSpace M (χ - χ (LieAlgebra.IsKilling.coroot α) • ⇑α) = ⊥ ↔ LieModule.weightSpace M χ = ⊥

The set of weights is stable under the reflections. A form χ on the Cartan subalgebra is a weight of a finite-dimensional module exactly when its reflection s_α χ is.

Invariance under the Weyl group

@[simp]

theorem Ado.finrank_weightSpace_rootSystem_reflection {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (i : ↥LieSubalgebra.root) (χ : Module.Dual K ↥H) : Module.finrank K ↥(LieModule.weightSpace M ⇑(((LieAlgebra.IsKilling.rootSystem H).reflection i) χ)) = Module.finrank K ↥(LieModule.weightSpace M ⇑χ)

The reflections of the root system preserve weight multiplicities.

@[simp]

theorem Ado.finrank_weightSpace_weylGroup_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) (χ : Module.Dual K ↥H) : Module.finrank K ↥(LieModule.weightSpace M ⇑(w • χ)) = Module.finrank K ↥(LieModule.weightSpace M ⇑χ)

Weyl invariance of the weight multiplicities. For a finite-dimensional module M over a Killing-semisimple Lie algebra, the function χ ↦ dim Mχ on the dual Module.Dual K H is invariant under the Weyl group of the root system of H.

This is the direct, rank-one proof: it descends through Ado.finrank_weightSpace_sub_apply_coroot_smul to the sl₂ triple attached to each root, and so is available before — and independently of — Weyl's complete reducibility theorem.

@[simp]

theorem Ado.weightSpace_weylGroup_smul_eq_bot_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) (χ : Module.Dual K ↥H) : LieModule.weightSpace M ⇑(w • χ) = ⊥ ↔ LieModule.weightSpace M ⇑χ = ⊥

The set of weights is stable under the Weyl group. A form χ on the Cartan subalgebra is a weight of a finite-dimensional module exactly when its translate w • χ under an element of the Weyl group is.