Lie invariants of symmetric algebras are invariant under inner and grading automorphisms

A Lie algebra L acts on the symmetric algebra S(M) of a Lie module M by derivations, and TauCeti.SymmetricAlgebra.lieInvariants is the subalgebra they kill. If x : L acts nilpotently on M, the derivation by which it acts is the derivation induced by the nilpotent endomorphism ⁅x, -⁆ of M, so the algebra automorphism of S(M) induced by exp ⁅x, -⁆ fixes every Lie invariant.

For the adjoint module M = L and for the coadjoint module M = L* the automorphisms exp (ad x) and their transposes generate the actions of the group Int L = TauCeti.intLieAlgebra of inner automorphisms on S(L) and on the polynomial functions S(L*) on L. Therefore:

• the Lie invariants S(L)^L are invariant under Int L acting on S(L);
• the Lie invariants S(L*)^L are invariant under Int L acting on S(L*) through the contragredient representation, so an L-invariant polynomial function p on L satisfies p (g x) = p x for every inner automorphism g.

The second statement is what Chevalley's restriction theorem needs to apply the density of the conjugates of a Cartan subalgebra under Int L (LieSubalgebra.polynomial_eq_zero_of_invariant_of_cartan) to Lie-invariant polynomial functions, such as the trace-power polynomials TauCeti.tracePowerPolynomial.

Invariance also holds for the grading automorphisms TauCeti.gradingAut hh s, which act on the integer eigenspaces L(j) of ad h by s ^ j and are the adjoint action of the cocharacter integrating h when there is one. Over a field that is not algebraically closed these need not be inner, so this does not follow from the previous paragraph. Instead, the integer eigenspaces of the coadjoint action of h span L* (TauCeti.LieModule.iSup_eigenspace_toEnd_dual_eq_top), the transpose of gradingAut hh s acts on the weight j functionals by s⁻¹ ^ j, and an element of S(L*) killed by h has weight zero for the induced decomposition (SymmetricAlgebra.map_apply_of_derivationOfEnd_eq_smul).

Main results

• TauCeti.SymmetricAlgebra.map_exp_toEnd_apply_of_mem_lieInvariants: if x acts nilpotently on M, then exp ⁅x, -⁆ fixes the Lie invariants of S(M).
• TauCeti.SymmetricAlgebra.map_apply_of_mem_intLieAlgebra: an inner automorphism fixes the Lie invariants of S(L).
• TauCeti.SymmetricAlgebra.map_dualMap_apply_of_mem_intLieAlgebra: the transpose of an inner automorphism fixes the Lie invariants of S(L*).
• TauCeti.SymmetricAlgebra.lift_eval_smul_of_mem_intLieAlgebra: a Lie-invariant polynomial function on L is invariant under the inner automorphisms.
• TauCeti.SymmetricAlgebra.map_dualMap_gradingAut_apply and TauCeti.SymmetricAlgebra.lift_eval_gradingAut_apply: the transposes of the grading automorphisms attached to h fix the elements of S(L*) killed by h, so a polynomial function on L killed by h is invariant under the grading automorphisms.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1, where the polynomial functions on L invariant under Int L are those killed by the derivations ad x.

theorem TauCeti.SymmetricAlgebra.map_exp_toEnd_apply_of_mem_lieInvariants {K : Type u} {L : Type v} [CommRing K] [Algebra ℚ K] [LieRing L] [LieAlgebra K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [Module ℚ M] {x : L} (hx : IsNilpotent ((LieModule.toEnd K L M) x)) {p : SymmetricAlgebra K M} (hp : p ∈ lieInvariants K L M) : (SymmetricAlgebra.map K (IsNilpotent.exp ((LieModule.toEnd K L M) x))) p = p

Lie invariants are fixed by exponentials. If x acts nilpotently on M, the algebra automorphism of S(M) induced by exp ⁅x, -⁆ fixes every Lie invariant.

theorem TauCeti.SymmetricAlgebra.map_apply_of_mem_intLieAlgebra {K : Type u} {L : Type v} [CommRing K] [Algebra ℚ K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {g : LinearMap.GeneralLinearGroup K L} (hg : g ∈ intLieAlgebra K L) {p : SymmetricAlgebra K L} (hp : p ∈ lieInvariants K L L) : (SymmetricAlgebra.map K ↑g) p = p

Inner automorphisms fix the Lie invariants of S(L). The algebra automorphism of the symmetric algebra S(L) induced by an element of Int L fixes every element killed by the adjoint action of L.

theorem TauCeti.SymmetricAlgebra.map_dualMap_apply_of_mem_intLieAlgebra {K : Type u} {L : Type v} [CommRing K] [Algebra ℚ K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {g : LinearMap.GeneralLinearGroup K L} (hg : g ∈ intLieAlgebra K L) {p : SymmetricAlgebra K (Module.Dual K L)} (hp : p ∈ lieInvariants K L (Module.Dual K L)) : (SymmetricAlgebra.map K (↑g).dualMap) p = p

The transposes of inner automorphisms fix the Lie invariants of S(L*). The algebra automorphism of the polynomial functions S(L*) on L induced by the transpose of an element of Int L fixes every element killed by the coadjoint action of L.

theorem TauCeti.SymmetricAlgebra.lift_eval_smul_of_mem_intLieAlgebra {K : Type u} {L : Type v} [CommRing K] [Algebra ℚ K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {g : LinearMap.GeneralLinearGroup K L} (hg : g ∈ intLieAlgebra K L) {p : SymmetricAlgebra K (Module.Dual K L)} (hp : p ∈ lieInvariants K L (Module.Dual K L)) (x : L) : (SymmetricAlgebra.lift ((Module.Dual.eval K L) (g • x))) p = (SymmetricAlgebra.lift ((Module.Dual.eval K L) x)) p

Lie-invariant polynomial functions are invariant under inner automorphisms. If p in the algebra S(L*) of polynomial functions on L is killed by the coadjoint action of L, then p (g x) = p x for every g ∈ Int L and every x : L.

theorem TauCeti.SymmetricAlgebra.map_dualMap_gradingAut_apply {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad K L) h).eigenspace ↑j) {p : SymmetricAlgebra K (Module.Dual K L)} (hp : ((lieModuleDerivation K L (Module.Dual K L)) h) p = 0) (s : Kˣ) : (SymmetricAlgebra.map K (↑(gradingAut hh s).toLinearEquiv).dualMap) p = p

The transposes of the grading automorphisms fix the polynomial functions killed by h. If L is the internal direct sum of the integer eigenspaces of ad h, then the algebra automorphism of S(L*) induced by the transpose of TauCeti.gradingAut hh s fixes every p killed by the coadjoint action of h, in particular every Lie invariant.

theorem TauCeti.SymmetricAlgebra.lift_eval_gradingAut_apply {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad K L) h).eigenspace ↑j) {p : SymmetricAlgebra K (Module.Dual K L)} (hp : ((lieModuleDerivation K L (Module.Dual K L)) h) p = 0) (s : Kˣ) (x : L) : (SymmetricAlgebra.lift ((Module.Dual.eval K L) ((gradingAut hh s) x))) p = (SymmetricAlgebra.lift ((Module.Dual.eval K L) x)) p

Polynomial functions killed by h are invariant under the grading automorphisms. If L is the internal direct sum of the integer eigenspaces of ad h and p ∈ S(L*) is killed by the coadjoint action of h, then p (gradingAut hh s x) = p x for every unit s and every x : L. This applies to every Lie-invariant polynomial function, although the grading automorphisms need not be inner over a field that is not algebraically closed.