Exponentials of nilpotent endomorphisms on a symmetric algebra

A linear endomorphism f of a module M acts on the symmetric algebra S(M) in two ways: by the algebra endomorphism SymmetricAlgebra.map f, and by the derivation SymmetricAlgebra.derivationOfEnd R M f extending it. When f is nilpotent the two are related by exponentiation. The derivation D_f is then locally nilpotent, because its iterates send the generator ι x to ι (fⁿ x) and the generators span S(M) as an algebra. Over a ℚ-algebra its Taylor exponential ∑ D_fⁿ / n! is an algebra endomorphism of S(M) (Derivation.taylorExp), and it is the map induced by the endomorphism exp f of M:

map (exp f) = exp D_f.

Consequently every element of S(M) killed by D_f is fixed by map (exp f). This is how infinitesimal invariance under a Lie algebra acting nilpotently passes to invariance under the corresponding unipotent automorphisms: for the adjoint action of a Lie algebra L, the exponentials exp (ad x) generate the group of inner automorphisms of L, whose invariant polynomial functions Chevalley's restriction theorem describes.

Main results

• SymmetricAlgebra.exists_iterate_derivationOfEnd_eq_zero: D_f is locally nilpotent when f is nilpotent.
• SymmetricAlgebra.taylorExp_derivationOfEnd: exp D_f = map (exp f).
• SymmetricAlgebra.map_exp_apply_of_derivationOfEnd_eq_zero: an element killed by D_f is fixed by map (exp f).

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §2.3, for exponentials of nilpotent derivations, and §23.1, where the invariance of polynomial functions under the inner automorphisms is used.
• G. Freudenburg, Algebraic Theory of Locally Nilpotent Derivations, Chapter 1, for the exponential of a locally nilpotent derivation.

theorem SymmetricAlgebra.exists_iterate_derivationOfEnd_eq_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (hf : IsNilpotent f) (p : SymmetricAlgebra R M) : ∃ (n : ℕ), (⇑((derivationOfEnd R M) f))^[n] p = 0

The derivation induced by a nilpotent endomorphism is locally nilpotent: some iterate of it kills each element of the symmetric algebra.

theorem SymmetricAlgebra.taylorExp_derivationOfEnd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module ℚ M] [Algebra ℚ (SymmetricAlgebra R M)] {f : Module.End R M} (hf : IsNilpotent f) : ((derivationOfEnd R M) f).taylorExp ⋯ = map R (IsNilpotent.exp f)

The exponential of the derivation induced by a nilpotent endomorphism f is the algebra map induced by exp f: exp D_f = map (exp f).

theorem SymmetricAlgebra.map_exp_apply_of_derivationOfEnd_eq_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module ℚ M] [Algebra ℚ R] {f : Module.End R M} (hf : IsNilpotent f) {p : SymmetricAlgebra R M} (hp : ((derivationOfEnd R M) f) p = 0) : (map R (IsNilpotent.exp f)) p = p

Infinitesimal invariants of a nilpotent endomorphism are fixed by its exponential. If the derivation induced by a nilpotent endomorphism f kills p, then the algebra map induced by exp f fixes p.