Local nilpotence of a derivation on generators

A derivation D of an algebra A is locally nilpotent when every element is killed by some iterate of D. The elements killed by an iterate of D are closed under sums and, by the Leibniz rule, under products, and they contain the scalars. So local nilpotence can be checked on a generating set of the algebra.

The argument uses only linearity and the Leibniz rule, so it is stated once for linear endomorphisms satisfying the Leibniz rule, over semirings and without associativity or commutativity for the product lemma. It specialises both to Mathlib's Derivation and to the derivations of noncommutative algebras in TauCeti.derivationLieAlgebra.

This is the form in which local nilpotence is verified for the invariant vector fields of nilpotent tangent vectors of matrix groups, where the coordinate algebra is generated by matrix entries and a few further coordinates.

Main results

• Module.End.pow_apply_mul_eq_zero_of_leibniz: if fⁿ x = 0 and fᵐ y = 0 for a Leibniz endomorphism f, then fⁿ⁺ᵐ (x * y) = 0.
• Module.End.exists_pow_apply_eq_zero_of_mem_adjoin_of_leibniz: local nilpotence of a Leibniz endomorphism on a set extends to the subalgebra it generates.
• Derivation.exists_iterate_mul_eq_zero: a product of elements killed by iterates of D is killed by an iterate of D.
• Derivation.exists_iterate_eq_zero_of_mem_adjoin: every element of the subalgebra generated by a set of elements killed by iterates of D is killed by an iterate of D.
• Derivation.exists_iterate_eq_zero_of_adjoin_eq_top: a derivation which is locally nilpotent on a generating set is locally nilpotent.

References

• G. Freudenburg, Algebraic Theory of Locally Nilpotent Derivations, Encyclopaedia of Mathematical Sciences 136, Springer (2006), §1.1.

theorem Module.End.pow_apply_mul_eq_zero_of_leibniz {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {f : End R A} (hf : ∀ (x y : A), f (x * y) = f x * y + x * f y) {x y : A} {n m : ℕ} (hx : (f ^ n) x = 0) (hy : (f ^ m) y = 0) : (f ^ (n + m)) (x * y) = 0

If powers n and m of a linear endomorphism satisfying the Leibniz rule kill the two factors, power n + m kills their product. Neither associativity nor commutativity of multiplication is required.

theorem Module.End.exists_pow_apply_eq_zero_of_mem_adjoin_of_leibniz {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {f : End R A} (hf : ∀ (x y : A), f (x * y) = f x * y + x * f y) (hf1 : f 1 = 0) {s : Set A} (hs : ∀ x ∈ s, ∃ (n : ℕ), (f ^ n) x = 0) {a : A} (ha : a ∈ Algebra.adjoin R s) : ∃ (n : ℕ), (f ^ n) a = 0

Local nilpotence of a linear endomorphism satisfying the Leibniz rule and killing 1, on a set of generators, extends to the subalgebra they generate.

theorem Derivation.exists_iterate_mul_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) {a b : A} (ha : ∃ (m : ℕ), (⇑D)^[m] a = 0) (hb : ∃ (n : ℕ), (⇑D)^[n] b = 0) : ∃ (k : ℕ), (⇑D)^[k] (a * b) = 0

A product of two elements killed by iterates of a derivation is killed by an iterate of the derivation.

theorem Derivation.exists_iterate_eq_zero_of_mem_adjoin {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) {s : Set A} (hs : ∀ x ∈ s, ∃ (n : ℕ), (⇑D)^[n] x = 0) {a : A} (ha : a ∈ Algebra.adjoin R s) : ∃ (n : ℕ), (⇑D)^[n] a = 0

Every element of the subalgebra generated by elements killed by iterates of a derivation is itself killed by an iterate of the derivation.

theorem Derivation.exists_iterate_eq_zero_of_adjoin_eq_top {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) {s : Set A} (hgen : Algebra.adjoin R s = ⊤) (hs : ∀ x ∈ s, ∃ (n : ℕ), (⇑D)^[n] x = 0) (a : A) : ∃ (n : ℕ), (⇑D)^[n] a = 0

Local nilpotence can be checked on generators. A derivation which is locally nilpotent on a set of generators of the algebra is locally nilpotent.