Partial derivatives: the chain rule and vanishing derivatives

Partial derivatives commute with homomorphisms of polynomial algebras by the chain rule. If ∂f/∂xᵢ = 0, then each exponent of xᵢ occurring in f is zero in the coefficient ring. Below the characteristic this means that xᵢ does not occur in f.

Main results

• MvPolynomial.pderiv_algHom: the chain rule for a homomorphism of polynomial algebras.
• CharP.natCast_ne_zero_of_lt: a positive natural number below the characteristic is nonzero.
• MvPolynomial.coeff_mul_natCast_eq_zero_of_pderiv_eq_zero: the coefficient of m is annihilated by the exponent m i.
• MvPolynomial.notMem_vars_of_pderiv_eq_zero: a variable with vanishing partial derivative does not occur, when its exponents are nonzero in the coefficient ring.
• MvPolynomial.exists_pderiv_ne_zero: a nonconstant polynomial of total degree below the characteristic has a nonzero partial derivative.

theorem CharP.natCast_ne_zero_of_lt (R : Type u_1) [AddMonoidWithOne R] {p : ℕ} [CharP R p] {n : ℕ} (hn : n ≠ 0) (hnp : n < p) : ↑n ≠ 0

A positive natural number below the characteristic is nonzero.

theorem MvPolynomial.pderiv_algHom {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommRing K] [Fintype σ] (φ : MvPolynomial σ K →ₐ[K] MvPolynomial τ K) (f : MvPolynomial σ K) (k : τ) : (pderiv k) (φ f) = ∑ i : σ, φ ((pderiv i) f) * (pderiv k) (φ (X i))

The polynomial chain rule for a homomorphism of polynomial algebras.

theorem MvPolynomial.coeff_mul_natCast_eq_zero_of_pderiv_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {i : σ} (h : (pderiv i) f = 0) (m : σ →₀ ℕ) : f.coeff m * ↑(m i) = 0

If ∂f/∂xᵢ = 0, then the coefficient of f at m is annihilated by the exponent m i.

theorem MvPolynomial.notMem_vars_of_pderiv_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f : MvPolynomial σ R} {i : σ} (h : (pderiv i) f = 0) (hchar : ∀ (n : ℕ), 0 < n → n ≤ degreeOf i f → ↑n ≠ 0) : i ∉ f.vars

A variable with vanishing partial derivative does not occur in f, provided the positive natural numbers up to its degree are nonzero in R.

theorem MvPolynomial.exists_pderiv_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f : MvPolynomial σ R} (hpos : 0 < f.totalDegree) (hchar : ∀ (n : ℕ), 0 < n → n ≤ f.totalDegree → ↑n ≠ 0) : ∃ (i : σ), (pderiv i) f ≠ 0

A polynomial of positive total degree has a nonzero partial derivative, provided the positive natural numbers up to its total degree are nonzero in R.