Derivations vanish on algebraic elements in characteristic zero

Let S be a domain of characteristic zero and D a derivation of S vanishing on a subalgebra B. Then D vanishes on every element x algebraic over B. Indeed, if p is a nonzero polynomial over B of least degree with p(x) = 0, then D is B-linear and 0 = D (p(x)) = p'(x) · D x. In characteristic zero p' is nonzero, since p is not constant, and it has smaller degree, so p'(x) ≠ 0 and hence D x = 0.

The characteristic hypothesis cannot be dropped: in characteristic q the derivation d/dX of 𝔽_q[X] vanishes on the subalgebra 𝔽_q[X^q], over which X is algebraic, but not on X.

This is the algebraic input to the nonvanishing of the Jacobian determinant of a family of polynomials over which the polynomial ring is algebraic (SymmetricAlgebra.jacobian_ne_zero).

Main results

• Derivation.apply_eq_zero_of_isAlgebraic: in a domain of characteristic zero, a derivation vanishing on a subalgebra vanishes on every element algebraic over it.

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press (1990), Chapter 3, for this argument in the proof of the Jacobian criterion.

theorem Derivation.apply_eq_zero_of_isAlgebraic {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [CharZero S] [Algebra R S] (D : Derivation R S S) {B : Subalgebra R S} (hD : ∀ b ∈ B, D b = 0) {x : S} (hx : IsAlgebraic (↥B) x) : D x = 0

In a domain of characteristic zero, a derivation vanishing on a subalgebra B vanishes on every element algebraic over B.