Coefficient-wise derivation on polynomials #
In this file we define applying a derivation on the coefficients of a polynomial,
show this forms a derivation, and prove apply_eval_eq, which shows that for a derivation D,
D(p(x)) = (D.mapCoeffs p)(x) + D(x) * p'(x). apply_aeval_eq and apply_aeval_eq'
are generalizations of that for algebras.
def
Derivation.mapCoeffs
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
:
Derivation R (Polynomial A) (PolynomialModule A M)
The R-derivation from A[X] to M[X] which applies the derivative to each
of the coefficients.
Equations
- d.mapCoeffs = { toLinearMap := PolynomialModule.map A ↑d ∘ₗ ↑PolynomialModule.equivPolynomial.symm, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
Instances For
@[simp]
theorem
Derivation.mapCoeffs_apply
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
(p : Polynomial A)
(i : ℕ)
:
(d.mapCoeffs p) i = d (p.coeff i)
@[simp]
theorem
Derivation.mapCoeffs_monomial
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
(n : ℕ)
(x : A)
:
d.mapCoeffs ((Polynomial.monomial n) x) = (PolynomialModule.single A n) (d x)
@[simp]
theorem
Derivation.mapCoeffs_X
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
:
d.mapCoeffs Polynomial.X = 0
@[simp]
theorem
Derivation.mapCoeffs_C
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
(x : A)
:
d.mapCoeffs (Polynomial.C x) = (PolynomialModule.single A 0) (d x)
theorem
Derivation.apply_aeval_eq'
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
{B : Type u_4}
{M' : Type u_5}
[CommRing B]
[Algebra R B]
[Algebra A B]
[AddCommGroup M']
[Module B M']
[Module R M']
[Module A M']
(d' : Derivation R B M')
(f : M →ₗ[A] M')
(h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a))
(x : B)
(p : Polynomial A)
:
d' ((Polynomial.aeval x) p) = (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) + (Polynomial.aeval x) (Polynomial.derivative p) • d' x
theorem
Derivation.apply_aeval_eq
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
{B : Type u_4}
{M' : Type u_5}
[CommRing B]
[Algebra R B]
[Algebra A B]
[AddCommGroup M']
[Module B M']
[Module R M']
[Module A M']
[IsScalarTower R A B]
[IsScalarTower A B M']
(d : Derivation R B M')
(x : B)
(p : Polynomial A)
:
d ((Polynomial.aeval x) p) = (PolynomialModule.eval x) ((Derivation.compAlgebraMap A d).mapCoeffs p) + (Polynomial.aeval x) (Polynomial.derivative p) • d x
theorem
Derivation.apply_eval_eq
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(d : Derivation R A M)
(x : A)
(p : Polynomial A)
:
d (Polynomial.eval x p) = (PolynomialModule.eval x) (d.mapCoeffs p) + Polynomial.eval x (Polynomial.derivative p) • d x