Basic properties of derivations

A derivation vanishes on the image (n : A) of a natural number (Derivation.map_natCast). A numeric literal (OfNat.ofNat n : A) with 2 ≤ n is not syntactically such a cast, so simp does not apply that lemma to it. This file adds the literal form Derivation.map_ofNat, so that simp differentiates polynomial expressions with numeric coefficients, for instance partial derivatives MvPolynomial.pderiv i (3 * X 0 ^ 2).

A derivation differentiates a finite product termwise: D (∏ i ∈ s, f i) is the sum over j ∈ s of D (f j) times the product of the other factors. In particular, a derivation δ with δ tⱼ = δᵢⱼ sends a monomial ∏ⱼ tⱼ ^ βⱼ to βᵢ ∏ⱼ tⱼ ^ (β - eᵢ)ⱼ.

Iterates of a derivation remain linear over the scalars, so they commute with finite scalar linear combinations. On products they satisfy the general Leibniz rule Dⁿ (a * b) = ∑ (n choose i) Dⁱ a Dⁿ⁻ⁱ b.

An element whose derivative is a unit is squarefree, since a square factor x * x of a makes x divide D a. This detects squarefreeness of a polynomial from a partial derivative that is a unit, without factoring it.

Main results

• Derivation.map_ofNat: a derivation vanishes on numeric literals.
• Derivation.leibniz_prod: the Leibniz rule for finite products.
• Derivation.apply_prod_pow_of_apply_eq: a derivation dual to the i-th coordinate differentiates a monomial in the coordinates by lowering its i-th exponent.
• Derivation.iterate_sum_smul: iterated differentiation commutes with scalar linear combinations.
• Derivation.iterate_apply_mul: the general Leibniz rule for iterates of a derivation.
• Derivation.iterate_smul_apply: iterates of scalar multiples of a derivation.
• Derivation.exists_iterate_smul_eq_zero: scalar multiples preserve local nilpotence.
• Derivation.squarefree_of_isUnit: an element whose derivative is a unit is squarefree.

@[simp]

theorem Derivation.map_ofNat {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (n : ℕ) [n.AtLeastTwo] : D (OfNat.ofNat n) = 0

A derivation vanishes on numeric literals.

theorem Derivation.leibniz_prod {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) {ι : Type u_4} [DecidableEq ι] (s : Finset ι) (f : ι → A) : D (∏ i ∈ s, f i) = ∑ j ∈ s, (∏ i ∈ s.erase j, f i) • D (f j)

Leibniz rule for finite products: D (∏ i ∈ s, f i) is the sum over j ∈ s of D (f j) times the product of the other factors.

theorem Derivation.apply_prod_pow_of_apply_eq {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (δ : Derivation R A A) {t : ι → A} {i : ι} (ht : ∀ (j : ι), δ (t j) = if j = i then 1 else 0) (β : ι → ℕ) : δ (∏ j : ι, t j ^ β j) = β i • ∏ j : ι, t j ^ (β - Pi.single i 1) j

A derivation dual to the i-th coordinate differentiates a monomial ∏ⱼ tⱼ ^ βⱼ in the coordinates to βᵢ ∏ⱼ tⱼ ^ (β - eᵢ)ⱼ.

theorem Derivation.iterate_sum_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_4} (D : Derivation R A A) (m : ℕ) (s : Finset ι) (c : ι → R) (f : ι → A) : (⇑D)^[m] (∑ i ∈ s, c i • f i) = ∑ i ∈ s, c i • (⇑D)^[m] (f i)

Iterated differentiation commutes with finite scalar linear combinations.

theorem Derivation.iterate_apply_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) (n : ℕ) (a b : A) : (⇑D)^[n] (a * b) = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ((⇑D)^[ij.1] a * (⇑D)^[ij.2] b)

General Leibniz rule for iterates of a derivation of a commutative algebra.

The statement and proof are adapted from Mathlib's LieDerivation.iterate_apply_lie (Mathlib/Algebra/Lie/Derivation/Basic.lean).

theorem Derivation.iterate_smul_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) (r : R) (n : ℕ) (a : A) : (⇑(r • D))^[n] a = r ^ n • (⇑D)^[n] a

Iterating a scalar multiple of a derivation scales its iterates by the corresponding power.

theorem Derivation.exists_iterate_smul_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) (r : R) (a : A) : ∃ (n : ℕ), (⇑(r • D))^[n] a = 0

Scalar multiples of a locally nilpotent derivation are locally nilpotent.

theorem Derivation.squarefree_of_isUnit {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (D : Derivation R A A) {a : A} (ha : IsUnit (D a)) : Squarefree a

An element whose derivative is a unit is squarefree: if a = x * x * y, then x divides D a = x * D (x * y) + x * y * D x.