The lowest weight of an irreducible 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 irreducible L-module carrying a highest weight vector of dominant integral weight lam. This file identifies w₀ • lam as the lowest weight of M, w₀ being the longest element of the Weyl group.

The weights of M are stable under the Weyl group and lie below lam (TauCeti.sub_weylGroup_smul_mem_posRootCone_of_genWeightSpace_ne_bot_of_isHighestWeightVector), so applying w₀ — which carries the positive root cone to its negative (TauCeti.neg_smul_mem_posRootCone_longestElement) — shows that every weight of M lies above w₀ • lam. Since the positive root cone is pointed, nothing at all sits below w₀ • lam: subtracting a positive root from it leaves the weight support.

M is not assumed finite-dimensional here; the statements are about the weight support alone.

The dominance of the opposite weight -(w₀ • lam) is proved alongside, since it is the same computation with the opposition involution of the base and no module is involved.

Main results

• TauCeti.IsDominantIntegral.neg_longestElement_smul: -(w₀ • lam) is dominant integral when lam is, by the opposition involution of the base.
• TauCeti.sub_longestElement_smul_mem_posRootCone_of_genWeightSpace_ne_bot: w₀ • lam is the lowest weight, and TauCeti.genWeightSpace_longestElement_smul_sub_root_eq_bot is the form a construction below the lowest weight space consumes.

References

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

Dominance of the opposite weight

theorem TauCeti.IsDominantIntegral.neg_longestElement_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} (hlam : IsDominantIntegral b lam) : IsDominantIntegral b (-(longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam))

The opposite of a dominant integral weight is dominant integral. The opposition involution i ↦ -w₀ i permutes the simple roots (TauCeti.opposition_mem_support), and the value of -(w₀ • lam) on the coroot of αᵢ is the value of lam on the coroot of the opposite simple root.

The lowest weight

theorem TauCeti.sub_longestElement_smul_mem_posRootCone_of_genWeightSpace_ne_bot {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) {chi : Module.Dual K ↥H} (hchi : LieModule.genWeightSpace M ⇑chi ≠ ⊥) : chi - longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam ∈ posRootCone (LieAlgebra.IsKilling.rootSystem H) b

w₀ • lam is the lowest weight of an irreducible highest weight module. Every weight lies above it, in the sense that their difference is a nonnegative combination of the simple roots.

The weights of M are stable under the Weyl group and lie below lam; applying w₀, which negates the positive root cone, reverses the inequality.

theorem TauCeti.genWeightSpace_longestElement_smul_sub_root_eq_bot {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {v : M} [LieModule.IsIrreducible K L M] (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) {i : ↥LieSubalgebra.root} (hi : i ∈ posRoots (LieAlgebra.IsKilling.rootSystem H) b) : LieModule.genWeightSpace M (⇑(longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam) - ⇑(LieModule.Weight.toLinear K (↥H) L ↑i)) = ⊥

Nothing lies below the lowest weight. Subtracting a positive root from w₀ • lam leaves the weight support of M: the positive root cone is pointed, so a weight below the lowest one would give a positive root whose negative is again in the cone.