Nilpotent derivations on finite enveloping quotients

A locally nilpotent Lie derivation lifts to a locally nilpotent derivation of the universal enveloping algebra. On any stable quotient that is finitely generated as a module over the coefficient ring, the induced derivation is nilpotent with a uniform bound. In particular this applies to finite-dimensional stable quotients over a field.

The enveloping algebra itself need not have a uniform bound: in characteristic zero, the lift of x ↦ y, y ↦ 0 on a two-dimensional abelian Lie algebra is y ∂/∂x on the polynomial algebra and has no uniform nilpotence bound. The finite-quotient statement supplies the derivation part of the multiplication-plus-derivation representations of split Lie extensions.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, Proposition E.5, for nilpotent derivations on finite enveloping quotients.

theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_pow_apply_ι (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (x : L) : (↑(envelopingDerivation R L D) ^ n) ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) ((↑D ^ n) x)

Powers of a lifted derivation agree on canonical generators with powers of the original Lie derivation.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.envelopingDerivation_pow_apply_ι' (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (n : ℕ) (x : L) : (↑(envelopingDerivation R L D) ^ n) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) ((↑D ^ n) x))

The simp-normal form of envelopingDerivation_pow_apply_ι, stated for the canonical generators as simp writes them.

theorem Ado.UniversalEnvelopingAlgebra.exists_envelopingDerivation_pow_apply_eq_zero (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (hD : ∀ (x : L), ∃ (n : ℕ), (↑D ^ n) x = 0) (a : UniversalEnvelopingAlgebra R L) : ∃ (n : ℕ), (↑(envelopingDerivation R L D) ^ n) a = 0

A Lie derivation that kills each vector after finitely many iterations has a locally nilpotent lift to the enveloping algebra. No finiteness assumption on the Lie algebra is needed.

theorem Ado.UniversalEnvelopingAlgebra.isNilpotent_envelopingDerivation_quotient (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (hD : ∀ (x : L), ∃ (n : ℕ), (↑D ^ n) x = 0) (J : Ideal (UniversalEnvelopingAlgebra R L)) [J.IsTwoSided] [Module.Finite R (UniversalEnvelopingAlgebra R L ⧸ J)] (hJ : envelopingDerivation R L D ∈ stableDerivations R (Submodule.restrictScalars R J)) : IsNilpotent ↑((derivationQuotientHom R J) ⟨envelopingDerivation R L D, hJ⟩)

A locally nilpotent Lie derivation induces a nilpotent operator on every stable enveloping quotient that is finitely generated as a module over the coefficient ring.