Derivations and ideals

A derivation D : A → M satisfies the Leibniz rule D (a * b) = a • D b + b • D a, so it maps the power I ^ (n + 1) of an ideal I of A into I ^ n • M. This is what makes every derivation continuous for the I-adic topologies. For n = 1, it maps the square I ^ 2 into I • M; in particular, an element f of an ideal I with D f ∉ I does not lie in I ^ 2.

This is the elementary half of the Jacobian criterion: if a partial derivative of f does not vanish at a point, then f is not in the square of the maximal ideal there. When the ambient local ring at the point is regular, f is therefore a regular parameter and the hypersurface f = 0 is regular at the point.

A derivation also vanishes on an ideal generated by elements on which it vanishes, provided those generators annihilate the target module. This applies in particular to derivations at a point and generators vanishing at that point.

Main results

• Derivation.apply_mem_pow_smul_top_of_mem_pow_succ: a derivation maps I ^ (n + 1) into I ^ n • M.
• Derivation.apply_mem_smul_top_of_mem_sq: a derivation maps I ^ 2 into I • M.
• Derivation.apply_mem_of_mem_sq: a derivation of A into itself maps I ^ 2 into I.
• Derivation.apply_eq_zero_of_mem_span: vanishing on generators that annihilate the target extends to their ideal span.

theorem Derivation.apply_eq_zero_of_mem_span {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) {S : Set A} (hsmul : ∀ a ∈ S, ∀ (m : M), a • m = 0) (hd : ∀ a ∈ S, D a = 0) {x : A} (hx : x ∈ Ideal.span S) : D x = 0

A derivation which vanishes on generators that annihilate its target module vanishes on the ideal they generate.

theorem Derivation.apply_mem_pow_smul_top_of_mem_pow_succ {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) {I : Ideal A} {n : ℕ} {x : A} (hx : x ∈ I ^ (n + 1)) : D x ∈ I ^ n • ⊤

A derivation maps the power I ^ (n + 1) of an ideal I into I ^ n • M.

theorem Derivation.apply_mem_smul_top_of_mem_sq {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] (D : Derivation R A M) {I : Ideal A} {x : A} (hx : x ∈ I ^ 2) : D x ∈ I • ⊤

A derivation maps the square of an ideal I into I • M.

theorem Derivation.apply_mem_of_mem_sq {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) {I : Ideal A} {x : A} (hx : x ∈ I ^ 2) : D x ∈ I

A derivation of A into itself maps the square of an ideal I into I.