Trace-power polynomials of a Lie module

Let L be a Lie algebra over a commutative ring R and M a Lie module which is free of finite rank over R. The symmetric algebra S(L*) of the dual of L is the algebra of polynomial functions on L: a point x : L evaluates p : S(L*) through SymmetricAlgebra.lift (Module.Dual.eval R L x). For each natural number m, the function x ↦ tr (ρ_M(x) ^ m) is such a polynomial function, the trace-power polynomial TauCeti.tracePowerPolynomial R L M m, homogeneous of degree m.

It is built from the generic action matrix of a basis c of M (TauCeti.genericActionMatrix): the matrix over S(L*) whose (p, q) entry is the linear function x ↦ (matrix of ρ_M(x) in c) p q. Evaluating it at x gives the matrix of ρ_M(x), so the trace of its m-th power evaluates to tr (ρ_M(x) ^ m). Changing the basis conjugates the generic action matrix by constant matrices, so this trace does not depend on the basis.

The trace-power polynomials are invariant under the coadjoint action of L on S(L*): they lie in S(L*)^L (TauCeti.tracePowerPolynomial_mem_lieInvariants). This is the polynomial form of tr (ρ(x) ^ m) = tr (ρ(g x) ^ m) for inner automorphisms g, and it holds over every commutative ring: the coadjoint derivation of y : L, applied entrywise, sends the generic action matrix A to the commutator A ρ(y) - ρ(y) A, hence each power A ^ m to A ^ m ρ(y) - ρ(y) A ^ m, whose trace vanishes.

For a semisimple Lie algebra over an algebraically closed field of characteristic zero, these invariant polynomials restrict on a Cartan subalgebra to the power sums of the weights of M, and they are the invariant polynomial functions used in the surjectivity half of Chevalley's restriction theorem and of the Harish-Chandra isomorphism.

Main definitions

• TauCeti.genericActionMatrix R L c: the generic action matrix of L on M in the basis c.
• TauCeti.tracePowerPolynomial R L M m: the polynomial function x ↦ tr (ρ_M(x) ^ m) on L, as an element of S(L*).

Main results

• TauCeti.map_lift_eval_genericActionMatrix: evaluating the generic action matrix at x gives the matrix of ρ_M(x).
• TauCeti.genericActionMatrix_eq_map_toMatrix_mul_mul: change of basis conjugates the generic action matrix.
• TauCeti.tracePowerPolynomial_eq_trace_pow_genericActionMatrix: the trace-power polynomial is the trace of the m-th power of the generic action matrix in any basis.
• TauCeti.lift_eval_tracePowerPolynomial: the value of the trace-power polynomial at x is tr (ρ_M(x) ^ m).
• TauCeti.tracePowerPolynomial_mem_homogeneousSubmodule: it is homogeneous of degree m.
• TauCeti.tracePowerPolynomial_mem_lieInvariants: it is invariant under the coadjoint action.
• TauCeti.isNilpotent_toEnd_of_forall_lift_eval_eq_zero: over a field of characteristic zero, if every invariant polynomial function with zero constant term vanishes at x, then x acts nilpotently on every finite-dimensional module, by the trace criterion.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1, where the functions x ↦ tr (ρ(x) ^ m) are the invariant polynomial functions used to prove the surjectivity of the restriction to a Cartan subalgebra.

The generic action matrix

noncomputable def TauCeti.genericActionMatrix (R : Type u_1) (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (c : Module.Basis κ R M) : Matrix κ κ (SymmetricAlgebra R (Module.Dual R L))

The generic action matrix of L on M in a basis c of M: the matrix over the algebra S(L*) of polynomial functions on L whose (p, q) entry is the linear function x ↦ (matrix of ρ_M(x) in c) p q. Evaluating it at x : L gives the matrix of ρ_M(x) (TauCeti.map_lift_eval_genericActionMatrix).

theorem TauCeti.genericActionMatrix_apply (R : Type u_1) (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (c : Module.Basis κ R M) (p q : κ) : genericActionMatrix R L c p q = (SymmetricAlgebra.ι R (Module.Dual R L)) (Matrix.entryLinearMap R R p q ∘ₗ ↑(LinearMap.toMatrix c c) ∘ₗ ↑(LieModule.toEnd R L M))

The (p, q) entry of the generic action matrix is the generator of S(L*) given by the linear function x ↦ (matrix of ρ_M(x) in c) p q.

@[simp]

theorem TauCeti.map_lift_eval_genericActionMatrix (R : Type u_1) (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (c : Module.Basis κ R M) (x : L) : (genericActionMatrix R L c).map ⇑(SymmetricAlgebra.lift ((Module.Dual.eval R L) x)) = (LinearMap.toMatrix c c) ((LieModule.toEnd R L M) x)

Evaluating the generic action matrix at x : L gives the matrix of ρ_M(x).

theorem TauCeti.genericActionMatrix_eq_map_toMatrix_mul_mul (R : Type u_1) (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] {κ' : Type u_5} [Fintype κ'] [DecidableEq κ'] (c : Module.Basis κ R M) (c' : Module.Basis κ' R M) : genericActionMatrix R L c' = (c'.toMatrix ⇑c).map ⇑(algebraMap R (SymmetricAlgebra R (Module.Dual R L))) * genericActionMatrix R L c * (c.toMatrix ⇑c').map ⇑(algebraMap R (SymmetricAlgebra R (Module.Dual R L)))

Change of basis conjugates the generic action matrix by the constant change-of-basis matrices.

theorem TauCeti.trace_pow_genericActionMatrix (R : Type u_1) (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] {κ' : Type u_5} [Fintype κ'] [DecidableEq κ'] (c : Module.Basis κ R M) (c' : Module.Basis κ' R M) (m : ℕ) : (genericActionMatrix R L c' ^ m).trace = (genericActionMatrix R L c ^ m).trace

The trace of a power of the generic action matrix does not depend on the basis.

theorem TauCeti.map_lieModuleDerivation_genericActionMatrix (R : Type u_1) (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (c : Module.Basis κ R M) (y : L) : (genericActionMatrix R L c).map ⇑((SymmetricAlgebra.lieModuleDerivation R L (Module.Dual R L)) y) = genericActionMatrix R L c * ((LinearMap.toMatrix c c) ((LieModule.toEnd R L M) y)).map ⇑(algebraMap R (SymmetricAlgebra R (Module.Dual R L))) - ((LinearMap.toMatrix c c) ((LieModule.toEnd R L M) y)).map ⇑(algebraMap R (SymmetricAlgebra R (Module.Dual R L))) * genericActionMatrix R L c

The coadjoint action on the generic action matrix. The derivation of S(L*) by which y : L acts, applied entrywise, sends the generic action matrix A to the commutator A ρ_M(y) - ρ_M(y) A with the constant matrix of ρ_M(y).

The trace-power polynomials

noncomputable def TauCeti.tracePowerPolynomial (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] (m : ℕ) : SymmetricAlgebra R (Module.Dual R L)

The trace-power polynomial of the Lie module M: the polynomial function x ↦ tr (ρ_M(x) ^ m) on L, as an element of the symmetric algebra S(L*) (TauCeti.lift_eval_tracePowerPolynomial). It is the trace of the m-th power of the generic action matrix of any basis of M (TauCeti.tracePowerPolynomial_eq_trace_pow_genericActionMatrix), and it is invariant under the coadjoint action of L (TauCeti.tracePowerPolynomial_mem_lieInvariants).

theorem TauCeti.tracePowerPolynomial_eq_trace_pow_genericActionMatrix {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] {κ : Type u_4} [Fintype κ] [DecidableEq κ] (c : Module.Basis κ R M) (m : ℕ) : tracePowerPolynomial R L M m = (genericActionMatrix R L c ^ m).trace

The trace-power polynomial is the trace of the m-th power of the generic action matrix in any basis of M.

@[simp]

theorem TauCeti.lift_eval_tracePowerPolynomial {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] (x : L) (m : ℕ) : (SymmetricAlgebra.lift ((Module.Dual.eval R L) x)) (tracePowerPolynomial R L M m) = (LinearMap.trace R M) ((LieModule.toEnd R L M) x ^ m)

The value of the trace-power polynomial at x : L is tr (ρ_M(x) ^ m).

theorem TauCeti.tracePowerPolynomial_mem_homogeneousSubmodule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] (m : ℕ) : tracePowerPolynomial R L M m ∈ SymmetricAlgebra.homogeneousSubmodule R (Module.Dual R L) m

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

theorem TauCeti.tracePowerPolynomial_mem_lieInvariants {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] (m : ℕ) : tracePowerPolynomial R L M m ∈ SymmetricAlgebra.lieInvariants R L (Module.Dual R L)

The trace-power polynomials are invariant under the coadjoint action of L on S(L*).

Nilpotence from vanishing invariants

theorem TauCeti.isNilpotent_toEnd_of_forall_lift_eval_eq_zero {K : Type u_4} {L : Type u_5} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] (M : Type u_6) [AddCommGroup M] [Module K M] [FiniteDimensional K M] [LieRingModule L M] [LieModule K L M] {x : L} (h : ∀ p ∈ SymmetricAlgebra.lieInvariants K L (Module.Dual K L), SymmetricAlgebra.algebraMapInv p = 0 → (SymmetricAlgebra.lift ((Module.Dual.eval K L) x)) p = 0) : IsNilpotent ((LieModule.toEnd K L M) x)

Vanishing invariants force nilpotence in every finite-dimensional module. If every invariant polynomial function on L with zero constant term vanishes at x, then x acts nilpotently on every finite-dimensional Lie module: the invariants include the trace-power polynomials x ↦ tr (ρ_M(x) ^ m).