Documentation

Mathlib.RingTheory.Derivation.MapCoeffs

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. We also have a special case for DifferentialAlgebras.

source
noncomputable 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.

Instances For
    source
    @[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).coeff i = d (p.coeff i)
    source
    @[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)
    source
    @[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
    source
    @[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)
    source
    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
    source
    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) ((PolynomialModule.map B LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)) + (Polynomial.aeval x) (Polynomial.derivative p) • d x
    source
    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
    source
    noncomputable def Differential.mapCoeffs {A : Type u_1} [CommRing A] [Differential A] :
    Derivation ℤ (Polynomial A) (Polynomial A)

    A specialization of Derivation.mapCoeffs for the case of a differential ring.

    Instances For
      source
      @[simp]
      theorem Differential.coeff_mapCoeffs {A : Type u_1} [CommRing A] [Differential A] (p : Polynomial A) (i : ℕ) :
      (mapCoeffs p).coeff i = (p.coeff i)′
      source
      @[simp]
      theorem Differential.mapCoeffs_monomial {A : Type u_1} [CommRing A] [Differential A] (n : ℕ) (x : A) :
      mapCoeffs ((Polynomial.monomial n) x) = (Polynomial.monomial n) x′
      source
      @[simp]
      theorem Differential.mapCoeffs_X {A : Type u_1} [CommRing A] [Differential A] :
      mapCoeffs Polynomial.X = 0
      source
      @[simp]
      theorem Differential.mapCoeffs_C {A : Type u_1} [CommRing A] [Differential A] (x : A) :
      mapCoeffs (Polynomial.C x) = Polynomial.C x′
      source
      theorem Differential.deriv_aeval_eq {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] (x : R) (p : Polynomial A) :
      ((Polynomial.aeval x) p)′ = (Polynomial.aeval x) (mapCoeffs p) + (Polynomial.aeval x) (Polynomial.derivative p) * x′
      source
      noncomputable def Differential.implicitDeriv {A : Type u_1} [CommRing A] [Differential A] (v : Polynomial A) :
      Derivation ℤ (Polynomial A) (Polynomial A)

      The unique derivation which can be made to a DifferentialAlgebra on A[X] with X′ = v.

      Instances For
        source
        @[simp]
        theorem Differential.implicitDeriv_C {A : Type u_1} [CommRing A] [Differential A] (v : Polynomial A) (b : A) :
        (implicitDeriv v) (Polynomial.C b) = Polynomial.C b′
        source
        @[simp]
        theorem Differential.implicitDeriv_X {A : Type u_1} [CommRing A] [Differential A] (v : Polynomial A) :
        (implicitDeriv v) Polynomial.X = v
        source
        theorem Differential.deriv_aeval_eq_implicitDeriv {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] (x : R) (v : Polynomial A) (h : x′ = (Polynomial.aeval x) v) (p : Polynomial A) :
        ((Polynomial.aeval x) p)′ = (Polynomial.aeval x) ((implicitDeriv v) p)
        source
        theorem Differential.algHom_deriv {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [CommRing R'] [Differential R'] [Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Nontrivial R] (f : R →ₐ[A] R') (hf : Function.Injective ⇑f) (x : R) (h : IsSeparable A x) :
        f x′ = (f x)′
        source
        theorem Differential.algEquiv_deriv {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [CommRing R'] [Differential R'] [Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] (f : R ≃ₐ[A] R') (x : R) (h : IsSeparable A x) :
        f x′ = (f x)′
        source
        theorem Differential.algHom_deriv' {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [CommRing R'] [Differential R'] [Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Nontrivial R] [Algebra.IsSeparable A R] (f : R →ₐ[A] R') (hf : Function.Injective ⇑f) (x : R) :
        f x′ = (f x)′

        algHom_deriv in a separable algebra

        source
        theorem Differential.algEquiv_deriv' {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [CommRing R'] [Differential R'] [Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Algebra.IsSeparable A R] (f : R ≃ₐ[A] R') (x : R) :
        f x′ = (f x)′

        algEquiv_deriv in a separable algebra