Local nilpotence of algebra derivations #
For a derivation of a possibly noncommutative algebra, the elements annihilated by some power are closed under multiplication. Consequently, local nilpotence can be checked on algebra generators.
These facts allow nilpotent Lie derivations to act nilpotently on finite stable quotients of universal enveloping algebras, even though the lifted derivations on the enveloping algebras need not have a uniform nilpotence bound.
References #
- W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, Proposition E.5, for the use of nilpotent derivations on finite enveloping quotients.
theorem
Ado.derivationLieAlgebra.pow_apply_mul_eq_zero
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[NonUnitalNonAssocRing A]
[Module R A]
[SMulCommClass R A A]
[IsScalarTower R A A]
(D : ↥(derivationLieAlgebra R A))
{x y : A}
{n m : ℕ}
(hx : (↑D ^ n) x = 0)
(hy : (↑D ^ m) y = 0)
:
If powers n and m of a derivation kill the two factors, power n + m kills their
product. Neither associativity nor commutativity of multiplication is required.
theorem
Ado.derivationLieAlgebra.exists_pow_apply_eq_zero_of_mem_adjoin
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[Ring A]
[Algebra R A]
(D : ↥(derivationLieAlgebra R A))
{s : Set A}
(hs : ∀ x ∈ s, ∃ (n : ℕ), (↑D ^ n) x = 0)
{a : A}
(ha : a ∈ Algebra.adjoin R s)
:
Local nilpotence on a set of generators extends to the algebra they generate.