The weights of an irreducible highest weight module are stable under the Weyl group

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 splitting Cartan subalgebra, let b be a base of its root system, and let M be an irreducible L-module carrying a highest weight vector of dominant integral weight lam. This file records that the weights of M are stable under the reflection in each simple root, hence under the whole Weyl group, and that they are integral on the simple coroots.

M is not assumed finite-dimensional: for the modules of Layer 4 of the highest weight roadmap finite-dimensionality is the conclusion, not a hypothesis. What is available instead is integrability along each simple root, proved in TauCeti/Algebra/Lie/HighestWeight/Integrable.lean, and reflection stability is what TauCeti/Algebra/Lie/Weights/Integrable.lean extracts from it. Combined with the weight cone lam - Q⁺ of TauCeti/Algebra/Lie/HighestWeight/Module.lean, stability under the reflections is what will confine the weights of M to a finite set.

Main results

• Ado.genWeightSpace_rootSystem_reflection_ne_bot: the weights of an irreducible highest weight module of dominant integral weight are stable under the reflection in a simple root.
• Ado.genWeightSpace_weylGroup_smul_ne_bot: the weights are stable under the whole Weyl group.
• Ado.genWeightSpace_weylGroup_smul_eq_bot_iff: a linear form is a nonweight exactly when each Weyl translate is a nonweight.
• Ado.sub_weylGroup_smul_mem_posRootCone_of_genWeightSpace_ne_bot_of_isHighestWeightVector: every point of the Weyl orbit of a weight remains below the highest weight in the positive root-cone order.
• Ado.exists_int_apply_coroot_of_genWeightSpace_ne_bot_of_isHighestWeightVector: those weights take integer values on the simple coroots.

References

This is the weight-stability half of the "weight-cone bound" milestone of Layer 4, "the classification of finite-dimensional irreducibles", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

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

theorem Ado.exists_int_apply_coroot_of_genWeightSpace_ne_bot_of_isHighestWeightVector {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {χ : ↥H → K} (hχ : LieModule.genWeightSpace M χ ≠ ⊥) : ∃ (m : ℤ), χ (LieAlgebra.IsKilling.coroot ↑i) = ↑m

The weights of an irreducible highest weight module are integral on the simple coroots. Let M be irreducible with a highest weight vector of dominant integral weight lam. Then every weight χ of M takes an integer value on the coroot of a simple root.

M is not assumed finite-dimensional; integrability along the simple root replaces that hypothesis.

theorem Ado.genWeightSpace_rootSystem_reflection_ne_bot {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {χ : Module.Dual K ↥H} (hχ : LieModule.genWeightSpace M ⇑χ ≠ ⊥) : LieModule.genWeightSpace M ⇑(((LieAlgebra.IsKilling.rootSystem H).reflection i) χ) ≠ ⊥

The weights of an irreducible highest weight module are stable under the simple reflections. Let M be irreducible with a highest weight vector of dominant integral weight lam, and let i be a simple root of the base b. Then the reflection s_i χ of a weight χ of M is again a weight of M.

M is not assumed finite-dimensional: it is integrable along i (Ado.locallyFiniteSubmodule_eq_top_of_isSl2Triple), which is what Ado.genWeightSpace_sub_apply_coroot_smul_ne_bot consumes. For a finite-dimensional module Ado.finrank_weightSpace_rootSystem_reflection gives the stronger conclusion that the reflection preserves the multiplicity, for every root and with no highest weight vector in sight.

theorem Ado.genWeightSpace_weylGroup_smul_ne_bot {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) {χ : Module.Dual K ↥H} (hχ : LieModule.genWeightSpace M ⇑χ ≠ ⊥) : LieModule.genWeightSpace M ⇑(w • χ) ≠ ⊥

The weights of an irreducible highest weight module are stable under the Weyl group. Let M be irreducible with a highest weight vector of dominant integral weight lam. If χ is a weight of M, then w • χ is a weight of M for every element w of the Weyl group.

The module is not assumed finite-dimensional.

theorem Ado.genWeightSpace_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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) (χ : Module.Dual K ↥H) : LieModule.genWeightSpace M ⇑(w • χ) = ⊥ ↔ LieModule.genWeightSpace M ⇑χ = ⊥

A linear form is not a weight of an irreducible highest weight module of dominant integral weight exactly when any Weyl translate is not a weight.

theorem Ado.sub_weylGroup_smul_mem_posRootCone_of_genWeightSpace_ne_bot_of_isHighestWeightVector {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) {χ : Module.Dual K ↥H} (hχ : LieModule.genWeightSpace M ⇑χ ≠ ⊥) : lam - w • χ ∈ posRootCone (LieAlgebra.IsKilling.rootSystem H) b

The Weyl orbit of every weight remains below the highest weight. If M is irreducible with a highest weight vector of dominant integral weight lam, then for every weight χ and every Weyl-group element w, the difference lam - w • χ belongs to the positive root cone.

This combines Weyl stability with the weight-cone theorem for highest weight modules.