Derivations preserve nilpotence in characteristic zero

Let D be a derivation of a commutative ring A, and let p be a prime ideal of A containing no positive integer, so that A ⧸ p has characteristic zero. Then D carries every nilpotent element of A into p. Over a ℚ-algebra every prime ideal qualifies, so a derivation of a ℚ-algebra carries nilpotent elements to nilpotent elements: the nilradical is a differential ideal.

The characteristic hypothesis cannot be dropped. Over 𝔽ₚ[t] ⧸ (tᵖ) the derivation d/dt sends the nilpotent class of t to 1.

These facts are the commutative-algebra input to Cartier's theorem that affine group schemes of finite type over a field of characteristic zero are smooth: a tangent vector at the identity extends to a derivation of the whole coordinate ring, and the result here shows that it must vanish on nilpotent functions.

Main results

• Derivation.apply_mem_of_isNilpotent: a derivation sends nilpotent elements into every prime ideal of residual characteristic zero.
• Derivation.isNilpotent_apply_of_isNilpotent: a derivation of a ℚ-algebra sends nilpotent elements to nilpotent elements.

References

• I. Kaplansky, An Introduction to Differential Algebra (1957), Chapter I: the radical of a differential ideal in a ring containing ℚ is differential.

theorem Derivation.apply_mem_of_isNilpotent {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] (D : Derivation R A A) {p : Ideal A} [hp : p.IsPrime] (hchar : ∀ (n : ℕ), ↑n ∈ p → n = 0) {x : A} (hx : IsNilpotent x) : D x ∈ p

A derivation sends nilpotent elements into every prime ideal of residual characteristic zero. The hypothesis hchar says that p contains no positive integer.

theorem Derivation.isNilpotent_apply_of_isNilpotent {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) {x : A} (hx : IsNilpotent x) : IsNilpotent (D x)

In a ℚ-algebra, a derivation sends nilpotent elements to nilpotent elements: the nilradical is a differential ideal.