feat(data/mv_polynomial/derivation): derivations of mv_polynomials (#…

…9145)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/mv_polynomial/basic.lean

@@ -125,6 +125,10 @@ instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] [distrib_mu
 add_monoid_algebra.is_central_scalar
 instance [comm_semiring R] [comm_semiring S₁] [algebra R S₁] : algebra R (mv_polynomial σ S₁) :=
 add_monoid_algebra.algebra
+-- Register with high priority to avoid timeout in `data.mv_polynomial.pderiv`
+instance is_scalar_tower' [comm_semiring R] [comm_semiring S₁] [algebra R S₁] :
+  is_scalar_tower R (mv_polynomial σ S₁) (mv_polynomial σ S₁) :=
+is_scalar_tower.right
 -- TODO[gh-6025]: make this an instance once safe to do so
 /-- If `R` is a subsingleton, then `mv_polynomial σ R` has a unique element -/
 protected def unique [comm_semiring R] [subsingleton R] : unique (mv_polynomial σ R) :=

src/data/mv_polynomial/derivation.lean

@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import data.mv_polynomial.supported
+import ring_theory.derivation
+
+/-!
+# Derivations of multivariate polynomials
+
+In this file we prove that a derivation of `mv_polynomial σ R` is determined by its values on all
+monomials `mv_polynomial.X i`. We also provide a constructor `mv_polynomial.mk_derivation` that
+builds a derivation from its values on `X i`s and a linear equivalence
+`mv_polynomial.equiv_derivation` between `σ → A` and `derivation (mv_polynomial σ R) A`.
+-/
+
+namespace mv_polynomial
+
+open_locale big_operators
+
+noncomputable theory
+
+variables {σ R A : Type*} [comm_semiring R] [add_comm_monoid A]
+  [module R A] [module (mv_polynomial σ R) A]
+
+section
+
+variable (R)
+
+/-- The derivation on `mv_polynomial σ R` that takes value `f i` on `X i`, as a linear map.
+Use `mv_polynomial.mk_derivation` instead. -/
+def mk_derivationₗ (f : σ → A) : mv_polynomial σ R →ₗ[R] A :=
+finsupp.lsum R $ λ xs : σ →₀ ℕ, (linear_map.ring_lmap_equiv_self R R A).symm $
+  xs.sum $ λ i k, monomial (xs - finsupp.single i 1) (k : R) • f i
+
+end
+
+lemma mk_derivationₗ_monomial (f : σ → A) (s : σ →₀ ℕ) (r : R) :
+  mk_derivationₗ R f (monomial s r) =
+    r • (s.sum $ λ i k, monomial (s - finsupp.single i 1) (k : R) • f i) :=
+sum_monomial_eq $ linear_map.map_zero _
+
+lemma mk_derivationₗ_C (f : σ → A) (r : R) : mk_derivationₗ R f (C r) = 0 :=
+(mk_derivationₗ_monomial f _ _).trans (smul_zero _)
+
+lemma mk_derivationₗ_X (f : σ → A) (i : σ) : mk_derivationₗ R f (X i) = f i :=
+(mk_derivationₗ_monomial f _ _).trans $ by simp
+
+@[simp] lemma derivation_C (D : derivation R (mv_polynomial σ R) A) (a : R) : D (C a) = 0 :=
+D.map_algebra_map a
+
+@[simp] lemma derivation_C_mul (D : derivation R (mv_polynomial σ R) A) (a : R)
+  (f : mv_polynomial σ R) : D (C a * f) = a • D f :=
+by rw [C_mul', D.map_smul]
+
+/-- If two derivations agree on `X i`, `i ∈ s`, then they agree on all polynomials from
+`mv_polynomial.supported R s`. -/
+lemma derivation_eq_on_supported {D₁ D₂ : derivation R (mv_polynomial σ R) A} {s : set σ}
+  (h : set.eq_on (D₁ ∘ X) (D₂ ∘ X) s) {f : mv_polynomial σ R} (hf : f ∈ supported R s) :
+  D₁ f = D₂ f :=
+derivation.eq_on_adjoin (set.ball_image_iff.2 h) hf
+
+lemma derivation_eq_of_forall_mem_vars {D₁ D₂ : derivation R (mv_polynomial σ R) A}
+  {f : mv_polynomial σ R} (h : ∀ i ∈ f.vars, D₁ (X i) = D₂ (X i)) :
+  D₁ f = D₂ f :=
+derivation_eq_on_supported h f.mem_supported_vars
+
+lemma derivation_eq_zero_of_forall_mem_vars {D : derivation R (mv_polynomial σ R) A}
+  {f : mv_polynomial σ R} (h : ∀ i ∈ f.vars, D (X i) = 0) : D f = 0 :=
+show D f = (0 : derivation R (mv_polynomial σ R) A) f,
+from derivation_eq_of_forall_mem_vars h
+
+@[ext] lemma derivation_ext {D₁ D₂ : derivation R (mv_polynomial σ R) A}
+  (h : ∀ i, D₁ (X i) = D₂ (X i)) :
+  D₁ = D₂ :=
+derivation.ext $ λ f, derivation_eq_of_forall_mem_vars (λ i _, h i)
+
+variables [is_scalar_tower R (mv_polynomial σ R) A]
+
+lemma leibniz_iff_X (D : mv_polynomial σ R →ₗ[R] A) (h₁ : D 1 = 0) :
+  (∀ p q, D (p * q) = p • D q + q • D p) ↔
+    (∀ s i, D (monomial s 1 * X i) = (monomial s 1 : mv_polynomial σ R) • D (X i) +
+      (X i : mv_polynomial σ R) • D (monomial s 1)) :=
+begin
+  refine ⟨λ H p i, H _ _, λ H, _⟩,
+  have hC : ∀ r, D (C r) = 0,
+  { intro r, rw [C_eq_smul_one, D.map_smul, h₁, smul_zero] },
+  have : ∀ p i, D (p * X i) = p • D (X i) + (X i : mv_polynomial σ R) • D p,
+  { intros p i,
+    induction p using mv_polynomial.induction_on' with s r p q hp hq,
+    { rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc,
+        smul_add, D.map_smul, smul_comm r (X i)], apply_instance },
+    { rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm] } },
+  intros p q,
+  induction q using mv_polynomial.induction_on,
+  case h_C : c { rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul,
+    C_eq_smul_one, smul_one_smul] },
+  case h_add : q₁ q₂ h₁ h₂ { simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul], abel },
+  case h_X : q i hq { simp only [this, ← mul_assoc, hq, mul_smul, smul_add, smul_comm (X i),
+      add_assoc] }
+end
+
+variables (R)
+
+/-- The derivation on `mv_polynomial σ R` that takes value `f i` on `X i`. -/
+def mk_derivation (f : σ → A) : derivation R (mv_polynomial σ R) A :=
+{ to_linear_map := mk_derivationₗ R f,
+  map_one_eq_zero' := mk_derivationₗ_C _ 1,
+  leibniz' := (leibniz_iff_X (mk_derivationₗ R f) (mk_derivationₗ_C _ 1)).2 $ λ s i,
+    begin
+      simp only [mk_derivationₗ_monomial, X, monomial_mul, one_smul, one_mul],
+      rw [finsupp.sum_add_index];
+        [skip, by simp, by { intros, simp only [nat.cast_add, (monomial _).map_add, add_smul] }],
+      rw [finsupp.sum_single_index, finsupp.sum_single_index]; [skip, by simp, by simp],
+      rw [tsub_self, add_tsub_cancel_right, nat.cast_one, ← C_apply, C_1, one_smul,
+        add_comm, finsupp.smul_sum],
+      refine congr_arg2 (+) rfl (finset.sum_congr rfl (λ j hj, _)), dsimp only,
+      rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le],
+      rwa [finsupp.single_le_iff, nat.succ_le_iff, pos_iff_ne_zero, ← finsupp.mem_support_iff]
+    end }
+
+@[simp] lemma mk_derivation_X (f : σ → A) (i : σ) : mk_derivation R f (X i) = f i :=
+mk_derivationₗ_X f i
+
+lemma mk_derivation_monomial (f : σ → A) (s : σ →₀ ℕ) (r : R) :
+  mk_derivation R f (monomial s r) =
+    r • (s.sum $ λ i k, monomial (s - finsupp.single i 1) (k : R) • f i) :=
+mk_derivationₗ_monomial f s r
+
+/-- `mv_polynomial.mk_derivation` as a linear equivalence. -/
+def mk_derivation_equiv : (σ → A) ≃ₗ[R] derivation R (mv_polynomial σ R) A :=
+linear_equiv.symm $
+{ inv_fun := mk_derivation R,
+  to_fun := λ D i, D (X i),
+  map_add' := λ D₁ D₂, rfl,
+  map_smul' := λ c D, rfl,
+  left_inv := λ D, derivation_ext $ mk_derivation_X _ _,
+  right_inv := λ f, funext $ mk_derivation_X _ _ }
+
+end mv_polynomial

src/data/mv_polynomial/pderiv.lean

@@ -1,12 +1,11 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Shing Tak Lam
+Authors: Shing Tak Lam, Yury Kudryashov
 -/
 
 import data.mv_polynomial.variables
-import algebra.module.basic
-import tactic.ring
+import data.mv_polynomial.derivation
 
 /-!
 # Partial derivatives of polynomials
@@ -18,7 +17,8 @@ It is based purely on the polynomial exponents and coefficients.
 
 ## Main declarations
 
-* `mv_polynomial.pderiv i p` : the partial derivative of `p` with respect to `i`.
+* `mv_polynomial.pderiv i p` : the partial derivative of `p` with respect to `i`, as a bundled
+  derivation of `mv_polynomial σ R`.
 
 ## Notation
 
@@ -41,135 +41,63 @@ This will give rise to a monomial in `mv_polynomial σ R` which mathematicians m
 
 noncomputable theory
 
-open_locale classical big_operators
+universes u v
 
-open set function finsupp add_monoid_algebra
-open_locale big_operators
+namespace mv_polynomial
 
-universes u
-variables {R : Type u}
 
-namespace mv_polynomial
-variables {σ : Type*} {a a' a₁ a₂ : R} {s : σ →₀ ℕ}
+open set function finsupp add_monoid_algebra
+open_locale classical big_operators
+
+variables {R : Type u} {σ : Type v} {a a' a₁ a₂ : R} {s : σ →₀ ℕ}
 
 section pderiv
 
 variables {R} [comm_semiring R]
 
 /-- `pderiv i p` is the partial derivative of `p` with respect to `i` -/
-def pderiv (i : σ) : mv_polynomial σ R →ₗ[R] mv_polynomial σ R :=
-{ to_fun := λ p, p.sum (λ A B, monomial (A - single i 1) (B * (A i))),
-  map_smul' := begin
-    intros c x,
-    rw [sum_smul_index', smul_sum],
-    { dsimp, simp_rw [← (monomial _).map_smul, smul_eq_mul, mul_assoc] },
-    { intros s,
-      simp only [monomial_zero, zero_mul] }
-  end,
-  map_add' := λ f g, sum_add_index (by simp only [monomial_zero, forall_const, zero_mul])
-    (by simp only [add_mul, forall_const, eq_self_iff_true, (monomial _).map_add]), }
-
-@[simp]
-lemma pderiv_monomial {i : σ} :
-  pderiv i (monomial s a) = monomial (s - single i 1) (a * (s i)) :=
-by simp only [pderiv, monomial_zero, sum_monomial_eq, zero_mul, linear_map.coe_mk]
+def pderiv (i : σ) : derivation R (mv_polynomial σ R) (mv_polynomial σ R) :=
+mk_derivation R $ pi.single i 1
 
+@[simp] lemma pderiv_monomial {i : σ} :
+  pderiv i (monomial s a) = monomial (s - single i 1) (a * (s i)) :=
+begin
+  simp only [pderiv, mk_derivation_monomial, finsupp.smul_sum, smul_eq_mul,
+    ← smul_mul_assoc, ← (monomial _).map_smul],
+  refine (finset.sum_eq_single i (λ j hj hne, _) (λ hi, _)).trans _,
+  { simp [pi.single_eq_of_ne hne] },
+  { rw [finsupp.not_mem_support_iff] at hi, simp [hi] },
+  { simp }
+end
 
-@[simp]
-lemma pderiv_C {i : σ} : pderiv i (C a) = 0 :=
-suffices pderiv i (monomial 0 a) = 0, by simpa,
-by simp only [monomial_zero, pderiv_monomial, nat.cast_zero, mul_zero, zero_apply]
+lemma pderiv_C {i : σ} : pderiv i (C a) = 0 := derivation_C _ _
 
-@[simp]
 lemma pderiv_one {i : σ} : pderiv i (1 : mv_polynomial σ R) = 0 := pderiv_C
 
-lemma pderiv_eq_zero_of_not_mem_vars {i : σ} {f : mv_polynomial σ R} (h : i ∉ f.vars) :
-  pderiv i f = 0 :=
-begin
-  change (pderiv i) f = 0,
-  rw [f.as_sum, linear_map.map_sum],
-  apply finset.sum_eq_zero,
-  intros x H,
-  simp [mem_support_not_mem_vars_zero H h],
-end
+@[simp] lemma pderiv_X [d : decidable_eq σ] (i j : σ) :
+  pderiv i (X j : mv_polynomial σ R) = @pi.single σ _ d _ i 1 j :=
+(mk_derivation_X _ _ _).trans (by congr)
 
-lemma pderiv_X [decidable_eq σ] {i j : σ} :
-  pderiv i (X j : mv_polynomial σ R) = if i = j then 1 else 0 :=
-begin
-  refine pderiv_monomial.trans _,
-  rcases eq_or_ne i j with (rfl|hne),
-  { simp },
-  { simp [hne, hne.symm] }
-end
+@[simp] lemma pderiv_X_self (i : σ) : pderiv i (X i : mv_polynomial σ R) = 1 := by simp
 
-@[simp] lemma pderiv_X_self {i : σ} : pderiv i (X i : mv_polynomial σ R) = 1 :=
-by simp [pderiv_X]
+@[simp] lemma pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv i (X j : mv_polynomial σ R) = 0 :=
+by simp [h]
+
+lemma pderiv_eq_zero_of_not_mem_vars {i : σ} {f : mv_polynomial σ R} (h : i ∉ f.vars) :
+  pderiv i f = 0 :=
+derivation_eq_zero_of_forall_mem_vars $ λ j hj, pderiv_X_of_ne $ ne_of_mem_of_not_mem hj h
 
 lemma pderiv_monomial_single {i : σ} {n : ℕ} :
   pderiv i (monomial (single i n) a) = monomial (single i (n-1)) (a * n) :=
 by simp
 
-private lemma monomial_sub_single_one_add {i : σ} {s' : σ →₀ ℕ} :
-  monomial (s - single i 1 + s') (a * (s i) * a') =
-    monomial (s + s' - single i 1) (a * (s i) * a') :=
-by by_cases h : s i = 0; simp [h, sub_single_one_add]
-
-private lemma monomial_add_sub_single_one {i : σ} {s' : σ →₀ ℕ} :
-  monomial (s + (s' - single i 1)) (a * (a' * (s' i))) =
-    monomial (s + s' - single i 1) (a * (a' * (s' i))) :=
-by by_cases h : s' i = 0; simp [h, add_sub_single_one]
-
-lemma pderiv_monomial_mul {i : σ} {s' : σ →₀ ℕ} :
-  pderiv i (monomial s a * monomial s' a') =
-    pderiv i (monomial s a) * monomial s' a' + monomial s a * pderiv i (monomial s' a') :=
-begin
-  simp only [monomial_sub_single_one_add, monomial_add_sub_single_one, pderiv_monomial,
-    pi.add_apply, monomial_mul, nat.cast_add, coe_add],
-  rw [mul_add, (monomial _).map_add, ← mul_assoc, mul_right_comm a _ a']
-end
-
-@[simp]
 lemma pderiv_mul {i : σ} {f g : mv_polynomial σ R} :
   pderiv i (f * g) = pderiv i f * g + f * pderiv i g :=
-begin
-  apply induction_on' f,
-  { apply induction_on' g,
-    { intros u r u' r', exact pderiv_monomial_mul },
-    { intros p q hp hq u r,
-      rw [mul_add, linear_map.map_add, hp, hq, mul_add, linear_map.map_add],
-      ring } },
-  { intros p q hp hq,
-    simp [add_mul, hp, hq],
-    ring, }
-end
+by simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm]
 
-@[simp]
-lemma pderiv_C_mul {f : mv_polynomial σ R} {i : σ} :
+@[simp] lemma pderiv_C_mul {f : mv_polynomial σ R} {i : σ} :
   pderiv i (C a * f) = C a * pderiv i f :=
-by convert linear_map.map_smul (pderiv i) a f; rw C_mul'
-
-@[simp]
-lemma pderiv_pow {i : σ} {f : mv_polynomial σ R} {n : ℕ} :
-  pderiv i (f^n) = n * pderiv i f * f^(n-1) :=
-begin
-  induction n with n ih,
-  { simp, },
-  { simp only [nat.succ_sub_succ_eq_sub, nat.cast_succ, tsub_zero, mv_polynomial.pderiv_mul,
-      pow_succ, ih],
-    cases n,
-    { simp, },
-    { simp only [nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, nat.cast_add, nat.cast_one,
-        pow_succ],
-      ring, }, },
-end
-
-@[simp]
-lemma pderiv_nat_cast {i : σ} {n : ℕ} : pderiv i (n : mv_polynomial σ R) = 0 :=
-begin
-  induction n with n ih,
-  { simp, },
-  { simp [ih], },
-end
+(derivation_C_mul _ _ _).trans C_mul'.symm
 
 end pderiv
 

src/ring_theory/derivation.lean

@@ -25,6 +25,7 @@ definitive definition of derivation will be implemented.
 -/
 
 open algebra
+open_locale big_operators
 
 /-- `D : derivation R A M` is an `R`-linear map from `A` to `M` that satisfies the `leibniz`
 equality. We also require that `D 1 = 0`. See `derivation.mk'` for a constructor that deduces this
@@ -86,6 +87,9 @@ protected lemma map_zero : D 0 = 0 := map_zero D
 @[simp] lemma map_smul : D (r • a) = r • D a := D.to_linear_map.map_smul r a
 @[simp] lemma leibniz : D (a * b) = a • D b + b • D a := D.leibniz' _ _
 
+lemma map_sum {ι : Type*} (s : finset ι) (f : ι → A) : D (∑ i in s, f i) = ∑ i in s, D (f i) :=
+D.to_linear_map.map_sum
+
 @[simp, priority 900] lemma map_smul_of_tower {S : Type*} [has_scalar S A] [has_scalar S M]
   [linear_map.compatible_smul A M S R] (D : derivation R A M) (r : S) (a : A) :
   D (r • a) = r • D a :=

src/ring_theory/polynomial/bernstein.lean

@@ -344,7 +344,7 @@ begin
   -- On the right hand side, we'll just simplify.
   conv at h
   { to_rhs,
-    rw [pderiv_pow, (pderiv tt).map_add, pderiv_tt_x, pderiv_tt_y],
+    rw [(pderiv tt).leibniz_pow, (pderiv tt).map_add, pderiv_tt_x, pderiv_tt_y],
     simp [e] },
   simpa using h,
 end
@@ -398,8 +398,8 @@ begin
   -- On the right hand side, we'll just simplify.
   conv at h
   { to_rhs,
-    simp only [pderiv_one, pderiv_mul, pderiv_pow, pderiv_nat_cast, (pderiv tt).map_add,
-      pderiv_tt_x, pderiv_tt_y],
+    simp only [pderiv_one, pderiv_mul, (pderiv _).leibniz_pow, (pderiv _).map_coe_nat,
+      (pderiv tt).map_add, pderiv_tt_x, pderiv_tt_y],
     simp [e, smul_smul] },
   simpa using h,
 end