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.

@[simp]

theorem Polynomial.derivative'_apply {R : Type u_1} [CommSemiring R] (a : Polynomial R) : Polynomial.derivative' a = Polynomial.derivative a

def Polynomial.derivative' {R : Type u_1} [CommSemiring R] : Derivation R (Polynomial R) (Polynomial R)

Polynomial.derivative as a derivation.

Equations

• Polynomial.derivative' = { toFun := ⇑Polynomial.derivative, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem Polynomial.derivation_C {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] (D : Derivation R (Polynomial R) A) (a : R) : D (Polynomial.C a) = 0

@[simp]

theorem Polynomial.C_smul_derivation_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] (D : Derivation R (Polynomial R) A) (a : R) (f : Polynomial R) : Polynomial.C a • D f = a • D f

theorem Polynomial.derivation_ext {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] {D₁ : Derivation R (Polynomial R) A} {D₂ : Derivation R (Polynomial R) A} (h : D₁ Polynomial.X = D₂ Polynomial.X) : D₁ = D₂

def Polynomial.mkDerivation (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] : A →ₗ[R] Derivation R (Polynomial R) A

The derivation on R[X] that takes the value a on X.

Equations

• Polynomial.mkDerivation R = { toFun := fun (a : A) => (LinearMap.toSpanSingleton (Polynomial R) A a).compDer Polynomial.derivative', map_add' := ⋯, map_smul' := ⋯ }

theorem Polynomial.mkDerivation_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (a : A) (f : Polynomial R) : ((Polynomial.mkDerivation R) a) f = Polynomial.derivative f • a

@[simp]

theorem Polynomial.mkDerivation_X (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (a : A) : ((Polynomial.mkDerivation R) a) Polynomial.X = a

theorem Polynomial.mkDerivation_one_eq_derivative' (R : Type u_1) [CommSemiring R] : (Polynomial.mkDerivation R) 1 = Polynomial.derivative'

theorem Polynomial.mkDerivation_one_eq_derivative (R : Type u_1) [CommSemiring R] (f : Polynomial R) : ((Polynomial.mkDerivation R) 1) f = Polynomial.derivative f

def Polynomial.mkDerivationEquiv (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] : A ≃ₗ[R] Derivation R (Polynomial R) A

Polynomial.mkDerivation as a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.mkDerivationEquiv_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (a : A) : (Polynomial.mkDerivationEquiv R) a = (Polynomial.mkDerivation R) a

@[simp]

theorem Polynomial.mkDerivationEquiv_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (D : Derivation R (Polynomial R) A) : (Polynomial.mkDerivationEquiv R).symm D = D Polynomial.X

@[simp]

theorem Derivation.compAEval_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (d : Derivation R A M) (a : A) (f : Polynomial R) : (d.compAEval a) f = (Module.AEval.of R M a) (d ((Polynomial.aeval a) f))

def Derivation.compAEval {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (d : Derivation R A M) (a : A) : Derivation R (Polynomial R) (Module.AEval R M a)

For a derivation d : A → M and an element a : A, d.compAEval a is the derivation of R[X] which takes a polynomial f to d(aeval a f).

This derivation takes values in Module.AEval R M a, which is M, regarded as an R[X]-module, with the action of a polynomial f defined by f • m = (aeval a f) • m.

Equations

• d.compAEval a = { toFun := fun (f : Polynomial R) => (Module.AEval.of R M a) (d ((Polynomial.aeval a) f)), map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

theorem Derivation.compAEval_eq {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R) : (d.compAEval a) f = Polynomial.derivative f • (Module.AEval.of R M a) (d a)

A form of the chain rule: if f is a polynomial over R and d : A → M is an R-derivation then for all a : A we have $$ d(f(a)) = f' (a) d a. $$ The equation is in the R[X]-module Module.AEval R M a. For the same equation in M, see Derivation.compAEval_eq.

theorem Derivation.comp_aeval_eq {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R) : d ((Polynomial.aeval a) f) = (Polynomial.aeval a) (Polynomial.derivative f) • d a

A form of the chain rule: if f is a polynomial over R and d : A → M is an R-derivation then for all a : A we have $$ d(f(a)) = f' (a) d a. $$ The equation is in M. For the same equation in Module.AEval R M a, see Derivation.compAEval_eq.