Weyl-alternating inversion of isotypic multiplicities

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. By Weyl's complete reducibility theorem, the formal character of a finite-dimensional L-module M is the multiplicity-weighted sum of the irreducible characters (TauCeti.formalCharacter_eq_finsum_isotypicMultiplicity_smul):

ch M = ∑_λ m_λ · ch L(λ).

This file proves that multiplication by the Weyl denominator Δ = ∏_{α>0}(1 - e^{-α}) inverts that expansion at the dominant integral weights: for a dominant integral weight ν, the coefficient of ch L(λ) · Δ at ν is 1 when λ = ν and 0 otherwise, so

[e^ν] (ch M · Δ) = m_ν,

reading the isotypic multiplicity m_ν = dim Hom_L(L(ν), M) off ch M by Weyl-alternating inversion (TauCeti.coeff_formalCharacter_mul_weylDenominator_eq_isotypicMultiplicity).

Main results

• TauCeti.coeff_irreducibleFormalCharacter_mul_weylDenominator_of_isDominantIntegral: orthogonality of irreducible characters against the Weyl denominator at dominant integral weights.
• TauCeti.coeff_formalCharacter_mul_weylDenominator_eq_isotypicMultiplicity: multiplication by the Weyl denominator reads off the isotypic multiplicities.

References

• N. Bourbaki, Groupes et algèbres de Lie, Ch. VIII, §9, Exercise 2 (the Brauer–Klimyk formula and its specialization to minuscule weights).
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. VI, §24, Exercise 9.

theorem TauCeti.coeff_irreducibleFormalCharacter_mul_weylDenominator_of_isDominantIntegral {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] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam : { l : Module.Dual K ↥H // IsDominantIntegral b l }) {nu : Module.Dual K ↥H} (hnu : IsDominantIntegral b nu) : (irreducibleFormalCharacter b lam * weylDenominator (LieAlgebra.IsKilling.rootSystem H) b).coeff nu = if ↑lam = nu then 1 else 0

Orthogonality of the irreducible characters against the Weyl denominator at dominant integral weights: for dominant integral lam and nu, the coefficient of ch L(lam) · Δ at nu is 1 when lam = nu and 0 otherwise.

theorem TauCeti.coeff_formalCharacter_mul_weylDenominator_eq_isotypicMultiplicity {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) [FiniteDimensional K M] {nu : Module.Dual K ↥H} (hnu : IsDominantIntegral b nu) : (formalCharacter K (↥H) M * weylDenominator (LieAlgebra.IsKilling.rootSystem H) b).coeff nu = ↑(LieModule.isotypicMultiplicity K L M (irreducibleQuotient b nu))

Weyl-alternating inversion of isotypic multiplicity: for any finite-dimensional L-module M and any dominant integral weight nu, the coefficient of ch M · Δ at nu is the multiplicity of L(nu) in M.

Expanding ch M = ∑_λ m_λ · ch L(λ) by TauCeti.formalCharacter_eq_finsum_isotypicMultiplicity_smul and multiplying by Δ, every summand λ ≠ ν vanishes at ν while the λ = ν summand has coefficient 1 there (TauCeti.coeff_irreducibleFormalCharacter_mul_weylDenominator_of_isDominantIntegral).