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
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
    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) 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) ((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
      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.

      Equations
        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
          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.

          Equations
            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