Trace-power polynomials on a Cartan subalgebra

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field K of characteristic zero, H a Cartan subalgebra and b a base of its root system. For a finite-dimensional module M and a natural number m, the function x ↦ tr (ρ_M(x) ^ m) is an invariant polynomial function on L. On H it is the power sum of the weights of M (TauCeti.trace_toEnd_pow_eq_sum_finrank_nsmul),

tr (ρ_M(h) ^ m) = ∑_μ dim M_μ · μ(h) ^ m,

which this file transports along the Killing duality H ≃ H* to an element of S(H), the algebra of polynomial functions on the weights. Writing t_μ ∈ H for the vector that represents a weight μ under the Killing form, it is

TauCeti.tracePowerRestriction K H M m = ∑_μ dim M_μ · t_μ ^ m,

whose value at a weight λ is ∑_μ dim M_μ ⟨λ, μ⟩ ^ m, with ⟨·,·⟩ = TauCeti.invForm. The main theorem is that these elements, for the irreducible modules L(λ) of the dominant integral weights λ, span the whole degree-m component of the Weyl invariants S(H)^W (TauCeti.linearInvariants). This is the Cartan-side input to the surjectivity half of Chevalley's restriction theorem: it says that every Weyl-invariant polynomial on H is a combination of the restrictions to H of the polynomial functions x ↦ tr (ρ_λ(x) ^ m) on L.

The proof combines three earlier results.

• Unitriangularity. The character of L(λ) is the Weyl orbit sum of λ plus a combination of the orbit sums of the dominant weights strictly below λ (TauCeti.formalCharacter_irreducibleQuotient_eq_orbitSum_add_lower). A downward induction on the finitely many dominant weights below λ therefore writes the power sum of every Weyl orbit of a dominant integral weight as a combination of the elements above.
• Density. The m-th powers of the vectors t_λ, for λ dominant integral, span the degree-m component of S(H) (TauCeti.span_pow_cartanEquivDual_symm_eq_homogeneousSubmodule); this is the polarization form of the polynomial density of the dominant integral weights.
• Averaging. The Reynolds operator of the Weyl group acting on H (Representation.symmetricAlgebraReynolds) sends t_λ ^ m to a multiple of the power sum of ∑_w e^{w λ}, because the form ⟨·,·⟩ is Weyl-invariant. That element is Weyl-invariant and supported on the Weyl orbit of λ, hence a combination of orbit sums, and the Reynolds operator fixes a Weyl invariant (TauCeti.linearInvariants_eq_symmetricAlgebraInvariants).

Main definitions

• TauCeti.weightPowerSum H m: the additive map ℤ[H*] → S(H) sending e^μ to t_μ ^ m.
• TauCeti.tracePowerRestriction K H M m: the degree-m power sum ∑_μ dim M_μ · t_μ ^ m of the weights of M.
• TauCeti.highestWeightTracePowerRestriction hlam m: the same for M = L(λ), λ dominant integral.

Main results

• TauCeti.lift_weightPowerSum: the value of weightPowerSum H m f at a weight λ is ∑_μ f(μ) ⟨λ, μ⟩ ^ m.
• TauCeti.weightPowerSum_mem_linearInvariants: a Weyl-invariant element of ℤ[H*] is sent to a Weyl invariant.
• TauCeti.lift_cartanEquivDual_tracePowerRestriction: the value of tracePowerRestriction K H M m at the weight κ(h, ·) is tr (ρ_M(h) ^ m), so it is the Killing transport of the restriction of x ↦ tr (ρ_M(x) ^ m) to H.
• TauCeti.map_dualMap_tracePowerPolynomial: the restriction to H of the invariant polynomial function TauCeti.tracePowerPolynomial K L M m on L is tracePowerRestriction K H M m, read through the Killing duality.
• TauCeti.lieCartanRestriction_killingSymmetricEquiv_symm_tracePowerPolynomial: the same on the side of S(L), where restriction to H is TauCeti.lieCartanRestriction.
• TauCeti.span_highestWeightTracePowerRestriction_eq_linearInvariants_inf_homogeneousSubmodule: the trace-power polynomials of the modules L(λ) span the degree-m Weyl invariants.

References

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

Power sums of weights

noncomputable def TauCeti.weightPowerSum {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (m : ℕ) : AddMonoidAlgebra ℤ (Module.Dual K ↥H) →+ SymmetricAlgebra K ↥H

The degree-m power sum of a weight function: the additive map ℤ[H*] → S(H) sending e^μ to t_μ ^ m, where t_μ ∈ H represents the weight μ under the Killing form. Read as a polynomial function on the weights, weightPowerSum H m f is λ ↦ ∑_μ f(μ) ⟨λ, μ⟩ ^ m (TauCeti.lift_weightPowerSum).

theorem TauCeti.weightPowerSum_apply {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (m : ℕ) (f : AddMonoidAlgebra ℤ (Module.Dual K ↥H)) : (weightPowerSum H m) f = f.coeff.sum fun (mu : Module.Dual K ↥H) (c : ℤ) => c • (SymmetricAlgebra.ι K ↥H) ((LieAlgebra.IsKilling.cartanEquivDual H).symm mu) ^ m

The power sum weightPowerSum H m f is ∑_μ f(μ) • t_μ ^ m.

@[simp]

theorem TauCeti.weightPowerSum_single {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (m : ℕ) (mu : Module.Dual K ↥H) (c : ℤ) : (weightPowerSum H m) (AddMonoidAlgebra.single mu c) = c • (SymmetricAlgebra.ι K ↥H) ((LieAlgebra.IsKilling.cartanEquivDual H).symm mu) ^ m

The power sum of a single weight e^μ is t_μ ^ m.

theorem TauCeti.lift_ι_cartanEquivDual_symm {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (lam mu : Module.Dual K ↥H) : (SymmetricAlgebra.lift lam) ((SymmetricAlgebra.ι K ↥H) ((LieAlgebra.IsKilling.cartanEquivDual H).symm mu)) = (invForm lam) mu

The vector t_μ representing a weight μ under the Killing form takes the value ⟨λ, μ⟩ at a weight λ.

theorem TauCeti.lift_weightPowerSum {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (lam : Module.Dual K ↥H) (m : ℕ) (f : AddMonoidAlgebra ℤ (Module.Dual K ↥H)) : (SymmetricAlgebra.lift lam) ((weightPowerSum H m) f) = f.coeff.sum fun (mu : Module.Dual K ↥H) (c : ℤ) => ↑c * (invForm lam) mu ^ m

The value of a power sum at a weight: weightPowerSum H m f takes the value ∑_μ f(μ) ⟨λ, μ⟩ ^ m at the weight λ.

theorem TauCeti.weightPowerSum_mem_homogeneousSubmodule {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (m : ℕ) (f : AddMonoidAlgebra ℤ (Module.Dual K ↥H)) : (weightPowerSum H m) f ∈ SymmetricAlgebra.homogeneousSubmodule K (↥H) m

A power sum of degree m is homogeneous of degree m.

Trace powers of a module

noncomputable def TauCeti.tracePowerRestriction (K : Type u) {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [CharZero K] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (m : ℕ) : SymmetricAlgebra K ↥H

The trace-power polynomial of a module on the Cartan subalgebra: the degree-m power sum ∑_μ dim M_μ · t_μ ^ m of the weights of M, counted with multiplicity, as an element of S(H). When K is algebraically closed, its value at the weight κ(h, ·) is tr (ρ_M(h) ^ m) (TauCeti.lift_cartanEquivDual_tracePowerRestriction), so it is the restriction to H of the invariant polynomial function x ↦ tr (ρ_M(x) ^ m) on L, transported along the Killing duality H ≃ H*. Without that hypothesis the formal character can miss the part of M on which H does not split, and the identification may fail.

theorem TauCeti.tracePowerRestriction_def {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (m : ℕ) : tracePowerRestriction K H M m = (weightPowerSum H m) (formalCharacter K (↥H) M)

The trace-power polynomial of M is the power sum of its formal character.

theorem TauCeti.tracePowerRestriction_mem_homogeneousSubmodule {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (m : ℕ) : tracePowerRestriction K H M m ∈ SymmetricAlgebra.homogeneousSubmodule K (↥H) m

A trace-power polynomial of degree m is homogeneous of degree m.

theorem TauCeti.lift_cartanEquivDual_tracePowerRestriction {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [IsAlgClosed K] (h : ↥H) (m : ℕ) : (SymmetricAlgebra.lift ((LieAlgebra.IsKilling.cartanEquivDual H) h)) (tracePowerRestriction K H M m) = (LinearMap.trace K M) ((LieModule.toEnd K (↥H) M) h ^ m)

The trace-power polynomial restricts the trace powers. The value of tracePowerRestriction K H M m at the weight κ(h, ·) represented by h ∈ H is tr (ρ_M(h) ^ m).

theorem TauCeti.map_dualMap_tracePowerPolynomial {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [IsAlgClosed K] (m : ℕ) : (SymmetricAlgebra.map K (↑H.incl).dualMap) (tracePowerPolynomial K L M m) = (SymmetricAlgebra.map K ↑(LieAlgebra.IsKilling.cartanEquivDual H)) (tracePowerRestriction K H M m)

The trace-power polynomial restricts to the power sum of the weights. Restricting the invariant polynomial function x ↦ tr (ρ_M(x) ^ m) on L (TauCeti.tracePowerPolynomial) to the Cartan subalgebra H gives the power sum tracePowerRestriction K H M m = ∑_μ dim M_μ · t_μ ^ m, read as a polynomial function on H through the Killing duality H ≃ H*.

theorem TauCeti.lieCartanRestriction_killingSymmetricEquiv_symm_tracePowerPolynomial {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [IsAlgClosed K] (m : ℕ) : (lieCartanRestriction H) ((killingSymmetricEquiv K L).symm (tracePowerPolynomial K L M m)) = tracePowerRestriction K H M m

The trace-power polynomial restricts to the power sum of the weights, on the side of S(L): transporting the invariant polynomial function x ↦ tr (ρ_M(x) ^ m) to S(L) along the Killing equivalence S(L) ≃ S(L*) and restricting it to S(H) by TauCeti.lieCartanRestriction gives tracePowerRestriction K H M m.

Weyl invariance

theorem TauCeti.weightPowerSum_mem_linearInvariants {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] (m : ℕ) {f : AddMonoidAlgebra ℤ (Module.Dual K ↥H)} (hf : IsWeylInvariant (LieAlgebra.IsKilling.rootSystem H) f) : (weightPowerSum H m) f ∈ linearInvariants H

The power sum of a Weyl-invariant weight function is a Weyl invariant.

theorem TauCeti.tracePowerRestriction_mem_linearInvariants {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (m : ℕ) : tracePowerRestriction K H M m ∈ linearInvariants H

A trace-power polynomial is a Weyl invariant, because the formal character is.

The trace-power polynomials of the irreducible modules span the Weyl invariants

noncomputable def TauCeti.highestWeightTracePowerRestriction {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} (hlam : IsDominantIntegral b lam) (m : ℕ) : SymmetricAlgebra K ↥H

The trace-power polynomial of L(λ) for a dominant integral weight λ, the module L(λ) being finite-dimensional exactly then (TauCeti.finiteDimensional_irreducibleQuotient_of_isDominantIntegral).

theorem TauCeti.highestWeightTracePowerRestriction_def {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} (hlam : IsDominantIntegral b lam) [FiniteDimensional K (irreducibleQuotient b lam)] (m : ℕ) : highestWeightTracePowerRestriction hlam m = tracePowerRestriction K H (irreducibleQuotient b lam) m

The trace-power polynomial of L(λ), for any choice of the finite-dimensionality instance.

theorem TauCeti.weightPowerSum_weightOrbitSum_mem_span {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} [IsAlgClosed K] [Finite ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] (m : ℕ) {lam : Module.Dual K ↥H} (hlam : IsDominantIntegral b lam) : (weightPowerSum H m) ((LieAlgebra.IsKilling.rootSystem H).weightOrbitSum lam) ∈ Submodule.span K {p : SymmetricAlgebra K ↥H | ∃ (mu : Module.Dual K ↥H) (hmu : IsDominantIntegral b mu), highestWeightTracePowerRestriction hmu m = p}

The orbit power sums lie in the span of the trace-power polynomials. For a dominant integral weight λ, the power sum of the Weyl orbit sum m_λ is a combination of the trace-power polynomials of the modules L(μ), μ dominant integral.

theorem TauCeti.weightPowerSum_sum_single_smul_mem_span {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} [IsAlgClosed K] [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] (m : ℕ) {lam : Module.Dual K ↥H} (hlam : IsDominantIntegral b lam) : (weightPowerSum H m) (∑ w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup, AddMonoidAlgebra.single (w • lam) 1) ∈ Submodule.span K {p : SymmetricAlgebra K ↥H | ∃ (mu : Module.Dual K ↥H) (hmu : IsDominantIntegral b mu), highestWeightTracePowerRestriction hmu m = p}

The Weyl-averaged power of a dominant weight lies in the span of the trace-power polynomials. For a dominant integral weight λ, the power sum of ∑_w e^{w λ}, in which each Weyl translate of λ occurs once for every Weyl group element, is a combination of the trace-power polynomials of the modules L(μ), μ dominant integral.

theorem TauCeti.span_highestWeightTracePowerRestriction_eq_linearInvariants_inf_homogeneousSubmodule {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [CharZero K] [LieModule.IsTriangularizable K (↥H) L] [IsAlgClosed K] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (m : ℕ) : Submodule.span K {p : SymmetricAlgebra K ↥H | ∃ (lam : Module.Dual K ↥H) (hlam : IsDominantIntegral b lam), highestWeightTracePowerRestriction hlam m = p} = Subalgebra.toSubmodule (linearInvariants H) ⊓ SymmetricAlgebra.homogeneousSubmodule K (↥H) m

The trace-power polynomials of the irreducible modules span the Weyl invariants. For every m, the trace-power polynomials tracePowerRestriction K H L(λ) m of the modules L(λ), λ dominant integral, span the degree-m component of the Weyl invariants S(H)^W.