The orbit-sum expansion of the character 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 Cartan subalgebra and b a base of its root system. For a finite-dimensional module M generated by a highest weight vector of weight lam (for instance the irreducible module L(lam) of a dominant integral weight), the formal character of M expands in the Weyl orbit sums m_mu = ∑_{nu ∈ W mu} e^nu as

ch M = m_lam + ∑_{mu < lam} c_mu m_mu,

the sum running over the dominant integral weights mu ≠ lam with lam - mu in the positive root cone, of which there are finitely many. The coefficient c_mu is the multiplicity of mu in M, a natural number (TauCeti.formalCharacter_coeff_nonneg), and the leading coefficient is 1. So the characters of the irreducible modules are unitriangular against the orbit sums with respect to the dominance order, which is what a downward induction on the dominant weights needs in order to pass between combinations of characters and combinations of orbit sums.

The expansion uses neither the Weyl character formula nor the Harish-Chandra theory. It is the orbit-sum expansion TauCeti.IsWeylInvariant.eq_sum_coeff_smul_weightOrbitSum of an arbitrary Weyl-invariant element of the integral group algebra, fed with three facts about the character of M: it is Weyl-invariant (TauCeti.isWeylInvariant_formalCharacter), supported in lam - Q⁺ on integral weights, and its coefficient at lam is 1, the top weight space being a line.

Main results

• TauCeti.mem_dominantWeightsBelow_iff_isDominantIntegral: the dominant integral weights below lam, in the Lie-theoretic language of TauCeti.IsDominantIntegral.
• TauCeti.formalCharacter_eq_orbitSum_add_lower: the orbit-sum expansion of the character of a highest weight module, ch M = m_lam + ∑_{mu < lam} c_mu m_mu.
• TauCeti.formalCharacter_irreducibleQuotient_eq_orbitSum_add_lower: the same expansion for L(lam).

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §22.5 and §23.1.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7-9, Ch. VIII, §7.

theorem TauCeti.mem_dominantWeightsBelow_iff_isDominantIntegral {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 mu : Module.Dual K ↥H} : mu ∈ (LieAlgebra.IsKilling.rootSystem H).dominantWeightsBelow b lam ↔ lam - mu ∈ posRootCone (LieAlgebra.IsKilling.rootSystem H) b ∧ IsDominantIntegral b mu

The dominant integral weights below lam are the dominant integral weights mu, in the sense of TauCeti.IsDominantIntegral, with lam - mu in the positive root cone.

theorem TauCeti.formalCharacter_eq_orbitSum_add_lower {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} [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [Finite ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) : formalCharacter K (↥H) M = (LieAlgebra.IsKilling.rootSystem H).weightOrbitSum lam + ∑ mu ∈ ((LieAlgebra.IsKilling.rootSystem H).dominantWeightsBelow b lam).erase lam, (formalCharacter K (↥H) M).coeff mu • (LieAlgebra.IsKilling.rootSystem H).weightOrbitSum mu

The orbit-sum expansion of the character of a highest weight module. Let M be a finite-dimensional module generated by a highest weight vector of weight lam. Then

ch M = m_lam + ∑_{mu} c_mu m_mu,

the sum running over the dominant integral weights mu ≠ lam below lam, where m_mu is the Weyl orbit sum of mu and c_mu is the multiplicity of the weight mu in M, a natural number by TauCeti.formalCharacter_coeff_nonneg.

Such an M is irreducible, by TauCeti.isIrreducible_of_isHighestWeightVector_of_lieSpan_eq_top, so this is the expansion of the character of L(lam); it is stated for M itself so that no identification with L(lam) is needed to use it.

theorem TauCeti.formalCharacter_irreducibleQuotient_eq_orbitSum_add_lower {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} [IsAlgClosed K] [Finite ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {lam : Module.Dual K ↥H} [FiniteDimensional K (irreducibleQuotient b lam)] : formalCharacter K (↥H) (irreducibleQuotient b lam) = (LieAlgebra.IsKilling.rootSystem H).weightOrbitSum lam + ∑ mu ∈ ((LieAlgebra.IsKilling.rootSystem H).dominantWeightsBelow b lam).erase lam, (formalCharacter K (↥H) (irreducibleQuotient b lam)).coeff mu • (LieAlgebra.IsKilling.rootSystem H).weightOrbitSum mu

The orbit-sum expansion of the character of L(lam): ch L(lam) = m_lam + ∑_{mu} c_mu m_mu, the sum running over the dominant integral weights mu ≠ lam below lam, with c_mu the multiplicity of mu in L(lam). The module L(lam) is finite-dimensional exactly when lam is dominant integral (TauCeti.finiteDimensional_irreducibleQuotient_of_isDominantIntegral).