feat: derivations of (univariate) polynomials (#6023)

An R-derivation from `R[X]` is determined by its value on `X`. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed `MvPolynomial.Derivation` .




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

Mathlib.lean

@@ -1659,6 +1659,7 @@ import Mathlib.Data.Polynomial.Degree.Definitions
 import Mathlib.Data.Polynomial.Degree.Lemmas
 import Mathlib.Data.Polynomial.Degree.TrailingDegree
 import Mathlib.Data.Polynomial.DenomsClearable
+import Mathlib.Data.Polynomial.Derivation
 import Mathlib.Data.Polynomial.Derivative
 import Mathlib.Data.Polynomial.Div
 import Mathlib.Data.Polynomial.EraseLead

Mathlib/Data/MvPolynomial/Derivation.lean

@@ -63,17 +63,11 @@ theorem derivation_C (D : Derivation R (MvPolynomial σ R) A) (a : R) : D (C a)
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.derivation_C MvPolynomial.derivation_C
 
--- @[simp] -- Porting note: simp normal form is `derivation_C_mul'`
-theorem derivation_C_mul (D : Derivation R (MvPolynomial σ R) A) (a : R) (f : MvPolynomial σ R) :
-    D (C a * f) = a • D f := by rw [C_mul', D.map_smul]
-set_option linter.uppercaseLean3 false in
-#align mv_polynomial.derivation_C_mul MvPolynomial.derivation_C_mul
-
 @[simp]
-theorem derivation_C_mul' (D : Derivation R (MvPolynomial σ R) A) (a : R) (f : MvPolynomial σ R) :
+theorem derivation_C_mul (D : Derivation R (MvPolynomial σ R) A) (a : R) (f : MvPolynomial σ R) :
     C (σ := σ) a • D f = a • D f := by
   have : C (σ := σ) a • D f = D (C a * f) := by simp
-  rw [this, derivation_C_mul]
+  rw [this, C_mul', D.map_smul]
 
 /-- If two derivations agree on `X i`, `i ∈ s`, then they agree on all polynomials from
 `MvPolynomial.supported R s`. -/

Mathlib/Data/MvPolynomial/PDeriv.lean

@@ -120,8 +120,8 @@ theorem pderiv_mul {i : σ} {f g : MvPolynomial σ R} :
 #align mv_polynomial.pderiv_mul MvPolynomial.pderiv_mul
 
 -- @[simp] -- Porting note: simp can prove this
-theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f :=
-  (derivation_C_mul _ _ _).trans C_mul'.symm
+theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f := by
+  rw [C_mul', Derivation.map_smul, C_mul']
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.pderiv_C_mul MvPolynomial.pderiv_C_mul
 

Mathlib/Data/Polynomial/Derivation.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2023 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard, Richard Hill
+-/
+import Mathlib.Data.Polynomial.Derivative
+import Mathlib.RingTheory.Derivation.Basic
+import Mathlib.Data.Polynomial.AlgebraMap
+
+/-!
+# Derivations of univariate polynomials
+
+In this file we prove that an `R`-derivation of `Polynomial R` is determined by its value on `X`.
+We also provide a constructor `Polynomial.mkDerivation` that
+builds a derivation from its value on `X`, and a linear equivalence
+`Polynomial.mkDerivationEquiv` between `A` and `Derivation (Polynomial R) A`.
+-/
+
+noncomputable section
+
+namespace Polynomial
+
+open scoped BigOperators
+
+variable {R A : Type _} [CommSemiring R]
+
+/-- `Polynomial.derivative` as a derivation. -/
+@[simps]
+def derivative' : Derivation R R[X] R[X] where
+  toFun := derivative
+  map_add' _ _ := derivative_add
+  map_smul' := derivative_smul
+  map_one_eq_zero' := derivative_one
+  leibniz' f g := by simp [mul_comm, add_comm, derivative_mul]
+
+variable [AddCommMonoid A] [Module R A] [Module (Polynomial R) A]
+
+@[simp]
+theorem derivation_C (D : Derivation R R[X] A) (a : R) : D (C a) = 0 :=
+  D.map_algebraMap a
+
+@[simp]
+theorem C_smul_derivation_apply (D : Derivation R R[X] A) (a : R) (f : R[X]) :
+    C a • D f = a • D f := by
+  have : C a • D f = D (C a * f) := by simp
+  rw [this, C_mul', D.map_smul]
+
+@[ext]
+theorem derivation_ext {D₁ D₂ : Derivation R R[X] A} (h : D₁ X = D₂ X) : D₁ = D₂ :=
+  Derivation.ext fun f => Derivation.eqOn_adjoin (Set.eqOn_singleton.2 h) <| by
+    simp only [adjoin_X, Algebra.coe_top, Set.mem_univ]
+
+variable [IsScalarTower R (Polynomial R) A]
+
+variable (R)
+
+/-- The derivation on `R[X]` that takes the value `a` on `X`. -/
+def mkDerivation : A →ₗ[R] Derivation R R[X] A where
+  toFun := fun a ↦ (LinearMap.toSpanSingleton R[X] A a).compDer derivative'
+  map_add' := fun a b ↦ by ext; simp
+  map_smul' := fun t a ↦ by ext; simp
+
+lemma mkDerivation_apply (a : A) (f : R[X]) :
+    mkDerivation R a f = derivative f • a := by
+  rfl
+
+@[simp]
+theorem mkDerivation_X (a : A) : mkDerivation R a X = a := by simp [mkDerivation_apply]
+
+lemma mkDerivation_one_eq_derivative' : mkDerivation R (1 : R[X]) = derivative' := by
+  ext : 1
+  simp [derivative']
+
+lemma mkDerivation_one_eq_derivative (f : R[X]) : mkDerivation R (1 : R[X]) f = derivative f := by
+  rw [mkDerivation_one_eq_derivative']
+  rfl
+
+/-- `Polynomial.mkDerivation` as a linear equivalence. -/
+def mkDerivationEquiv : A ≃ₗ[R] Derivation R R[X] A :=
+  LinearEquiv.symm <|
+    { invFun := mkDerivation R
+      toFun := fun D => D X
+      map_add' := fun _ _ => rfl
+      map_smul' := fun _ _ => rfl
+      left_inv := fun _ => derivation_ext <| mkDerivation_X _ _
+      right_inv := fun _ => mkDerivation_X _ _ }
+
+@[simp] lemma mkDerivationEquiv_apply (a : A) :
+    mkDerivationEquiv R a = mkDerivation R a := by
+  rfl
+
+@[simp] lemma mkDerivationEquiv_symm_apply (D : Derivation R R[X] A) :
+    (mkDerivationEquiv R).symm D = D X := rfl
+
+end Polynomial