From 30202c4ab3ac6242612cae3d3c2f957c11718229 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 2 Aug 2023 18:06:06 +0000 Subject: [PATCH] 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 Co-authored-by: Oliver Nash --- Mathlib.lean | 1 + Mathlib/Data/MvPolynomial/Derivation.lean | 10 +-- Mathlib/Data/MvPolynomial/PDeriv.lean | 4 +- Mathlib/Data/Polynomial/Derivation.lean | 95 +++++++++++++++++++++++ 4 files changed, 100 insertions(+), 10 deletions(-) create mode 100644 Mathlib/Data/Polynomial/Derivation.lean diff --git a/Mathlib.lean b/Mathlib.lean index e557d6c1614fc..0cb9af45ba47c 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Data/MvPolynomial/Derivation.lean b/Mathlib/Data/MvPolynomial/Derivation.lean index 7beaa92627892..37f73dc3e590a 100644 --- a/Mathlib/Data/MvPolynomial/Derivation.lean +++ b/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`. -/ diff --git a/Mathlib/Data/MvPolynomial/PDeriv.lean b/Mathlib/Data/MvPolynomial/PDeriv.lean index 6047d05f8394c..3224dd153add6 100644 --- a/Mathlib/Data/MvPolynomial/PDeriv.lean +++ b/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 diff --git a/Mathlib/Data/Polynomial/Derivation.lean b/Mathlib/Data/Polynomial/Derivation.lean new file mode 100644 index 0000000000000..185b381951667 --- /dev/null +++ b/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