The dominant integral weights are polynomially dense

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, let H be a splitting Cartan subalgebra and let b be a base of its root system. The symmetric algebra S(H) is the algebra of polynomial functions on the weights H*: a weight lam evaluates p : S(H) through SymmetricAlgebra.lift lam.

A polynomial function on the weights is determined by its values at the dominant integral weights alone. In the basis of H formed by the simple coroots, a weight has as coordinates its values on the simple coroots, and the dominant integral weights are exactly the weights whose coordinates are natural numbers. A polynomial vanishing on that box of natural numbers, which is infinite in every direction because K has characteristic zero, is zero.

By polarization, the n-th powers of the dominant integral weights therefore span the whole degree-n component of S(H*). This is the form in which the density is used to show that the restrictions to H of the trace polynomials x ↦ tr (ρ(x) ^ n) of the finite-dimensional representations span the Weyl-invariant polynomials, the surjectivity half of Chevalley's restriction theorem.

Main results

• TauCeti.polynomial_eq_zero_of_dominantIntegral: an element of S(H) vanishing at every dominant integral weight is zero.
• TauCeti.span_pow_eq_homogeneousSubmodule_of_isDominantIntegral: the n-th powers of the dominant integral weights span the degree-n component of S(H*).
• TauCeti.span_pow_cartanEquivDual_symm_eq_homogeneousSubmodule: the same in S(H), for the vectors t_λ ∈ H representing the dominant integral weights under the Killing form.

References

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

theorem TauCeti.polynomial_eq_zero_of_dominantIntegral {K : Type u_1} {L : Type u_2} [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) {p : SymmetricAlgebra K ↥H} (hp : ∀ (lam : Module.Dual K ↥H), IsDominantIntegral b lam → (SymmetricAlgebra.lift lam) p = 0) : p = 0

The dominant integral weights are polynomially dense. An element of the symmetric algebra S(H), viewed as a polynomial function on the weights H*, that vanishes at every dominant integral weight is zero.

theorem TauCeti.span_pow_eq_homogeneousSubmodule_of_isDominantIntegral {K : Type u_1} {L : Type u_2} [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) (n : ℕ) : Submodule.span K ((fun (lam : Module.Dual K ↥H) => (SymmetricAlgebra.ι K (Module.Dual K ↥H)) lam ^ n) '' {lam : Module.Dual K ↥H | IsDominantIntegral b lam}) = SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K ↥H) n

The powers of the dominant integral weights span each symmetric power of H*. The n-th powers of the dominant integral weights span the degree-n component of the symmetric algebra S(H*).

theorem TauCeti.span_pow_cartanEquivDual_symm_eq_homogeneousSubmodule {K : Type u_1} {L : Type u_2} [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) (n : ℕ) : Submodule.span K ((fun (lam : Module.Dual K ↥H) => (SymmetricAlgebra.ι K ↥H) ((LieAlgebra.IsKilling.cartanEquivDual H).symm lam) ^ n) '' {lam : Module.Dual K ↥H | IsDominantIntegral b lam}) = SymmetricAlgebra.homogeneousSubmodule K (↥H) n

The powers t_λ ^ n of the dominant integral weights span Sⁿ(H). Here t_λ ∈ H represents the weight λ under the Killing form; this is TauCeti.span_pow_eq_homogeneousSubmodule_of_isDominantIntegral transported along the Killing duality H ≃ H*.