The weight support of a highest weight 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 splitting Cartan subalgebra, let b be a base of its root system, and let M be an L-module carrying a highest weight vector of weight lam. This file describes the weights of M in two ways.

If M is irreducible and lam is dominant integral, M has only finitely many weights. M is not assumed finite-dimensional, and that is the whole point: for the modules L(lam) of Layer 4 of the highest weight roadmap, finite-dimensionality is the conclusion. Together with finite-dimensionality of the individual weight spaces it is what makes L(lam) finite-dimensional.

If instead M is finite-dimensional, every weight of M has a dominant integral Weyl conjugate which is again a weight of M. That is the form in which a weight of M is compared with lam, for example by the Casimir scalar in TauCeti/Algebra/Lie/HighestWeight/Separation.lean; dominance is what makes the invariant form available with a sign.

Main results

• Ado.finite_setOf_genWeightSpace_ne_bot_of_isHighestWeightVector: an irreducible highest weight module of dominant integral weight has finitely many weights.
• Ado.exists_weylGroup_smul_isDominantIntegral_of_genWeightSpace_ne_bot: every weight of a finite-dimensional highest weight module has a dominant integral Weyl conjugate, again a weight of the module.

The argument

Three facts about the weights of M are already available, none of them needing finite-dimensionality:

• they lie in the cone lam - Q⁺, by the weight-cone theorem of TauCeti/Algebra/Lie/HighestWeight/Module.lean;
• they take integer values on the simple coroots (Ado.exists_int_apply_coroot_of_genWeightSpace_ne_bot_of_isHighestWeightVector);
• they are stable under the simple reflections (Ado.genWeightSpace_rootSystem_reflection_ne_bot).

Ado.finite_of_forall_reflection_mem_of_sub_mem_posRootCone turns exactly that combination into finiteness, so the work here is to feed the three facts to it and then to remove the linearity restriction: a weight of M is a priori only a function H → K, but every weight of a highest weight module is of the form lam - ν, hence linear, by Ado.exists_sub_eq_of_genWeightSpace_ne_bot_of_isHighestWeightVector_of_lieSpan_eq_top.

The dominant conjugate comes from the same cone induction, used one step earlier: the raising step Ado.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone records which Weyl translate reaches a dominant member, and finiteness is its corollary. There the three facts are read off a finite-dimensional module instead, which needs neither irreducibility nor dominance of lam: the weights of such a module are Weyl stable (Ado.formalCharacter_coeff_weylGroup_smul) and integral (Ado.isIntegralWeight_of_formalCharacter_coeff_ne_zero).

References

This is the "weight-cone bound" milestone of Layer 4, "the classification of finite-dimensional irreducibles", of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, together with the dominant-conjugate step that Layer 7's "Freudenthal's multiplicity formula" needs.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §21.2, and §13.2 for the dominant conjugate.

theorem Ado.finite_setOf_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) : {chi : ↥H → K | LieModule.genWeightSpace M chi ≠ ⊥}.Finite

An irreducible highest weight module of dominant integral weight has finitely many weights. Let M be irreducible with a highest weight vector of dominant integral weight lam. Then only finitely many functions on the Cartan subalgebra have a nonzero weight space in M.

M is not assumed finite-dimensional. The three inputs — the weight cone lam - Q⁺, integrality on the simple coroots, and stability under the simple reflections — are exactly the hypotheses of Ado.finite_of_forall_reflection_mem_of_sub_mem_posRootCone, and each of them follows from hv, from dominance integrality of lam, and from irreducibility of M (used only through the resulting fact that v generates M).

theorem Ado.exists_weylGroup_smul_isDominantIntegral_of_genWeightSpace_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.IsTriangularizable K (↥H) L] [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) {mu : Module.Dual K ↥H} (hmu : LieModule.genWeightSpace M ⇑mu ≠ ⊥) : ∃ (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup), LieModule.genWeightSpace M ⇑(w • mu) ≠ ⊥ ∧ IsDominantIntegral b (w • mu)

Every weight of a finite-dimensional highest weight module has a dominant integral Weyl conjugate, again a weight of the module. Here M is a module over an algebraically closed field of characteristic zero, generated by a highest weight vector of weight lam, and M is not assumed irreducible.

The weights of a finite-dimensional module form a Weyl-stable set (Ado.formalCharacter_coeff_weylGroup_smul) of integral weights (Ado.isIntegralWeight_of_formalCharacter_coeff_ne_zero), and for a highest weight module they lie below the highest weight; that is exactly the input of Ado.exists_weylGroup_smul_dominant_of_forall_reflection_mem_of_sub_mem_posRootCone.