Documentation

TauCeti.RingTheory.PowerSeries.Derivation

Derivations of formal power series #

Let R be a commutative ring and M an R⟦X⟧-module which is Hausdorff for the X-adic topology, for instance R⟦X⟧ itself. This file shows that every R-derivation D : R⟦X⟧ → M is determined by its value at X, namely D f = f' • D X, so that m ↦ (f ↦ f' • m) is an R⟦X⟧-linear equivalence between M and Derivation R R⟦X⟧ M. In particular every derivation of R⟦X⟧ is a power-series multiple a • d⁄dX of the formal derivative. This holds in every characteristic and needs no continuity hypothesis.

Although R⟦X⟧ is not generated by X as an R-algebra, the value D X controls D through truncation. If D X = 0, then D vanishes on polynomials, and writing f = X ^ (n + 1) * g + trunc (n + 1) f gives D f = D (X ^ (n + 1) * g), which lies in X ^ n • M by the Leibniz rule (Derivation.apply_mem_pow_smul_top_of_mem_pow_succ). As this holds for every n, D f = 0 by the Hausdorff property. The same Leibniz estimate shows that every derivation is X-adically continuous (Derivation.continuous_adic).

This parallels Mathlib's Polynomial.derivation_ext and Polynomial.mkDerivationEquiv for derivations of R[X].

Main results #

source
theorem PowerSeries.derivation_coe {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] (D : Derivation R (PowerSeries R) M) (p : Polynomial R) :
D ↑p = ↑(Polynomial.derivative p) • D X

A derivation of R⟦X⟧ maps a polynomial p to p' • D X, by the chain rule for polynomials.

source
theorem Derivation.apply_eq_derivative_smul {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsHausdorff (Ideal.span {PowerSeries.X}) M] (D : Derivation R (PowerSeries R) M) (f : PowerSeries R) :
D f = PowerSeries.derivative f • D PowerSeries.X

A derivation D of R⟦X⟧ into an X-adically Hausdorff module is determined by its value at X: D f = f' • D X.

source
theorem PowerSeries.derivation_ext {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsHausdorff (Ideal.span {X}) M] {D₁ D₂ : Derivation R (PowerSeries R) M} (h : D₁ X = D₂ X) :
D₁ = D₂

Two derivations of R⟦X⟧ into an X-adically Hausdorff module which agree at X are equal.

source
theorem PowerSeries.derivation_ext_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsHausdorff (Ideal.span {X}) M] {D₁ D₂ : Derivation R (PowerSeries R) M} :
D₁ = D₂ ↔ D₁ X = D₂ X
source
noncomputable def PowerSeries.mkDerivation (R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsScalarTower R (PowerSeries R) M] :
M →ₗ[PowerSeries R] Derivation R (PowerSeries R) M

The derivation of R⟦X⟧ taking the value m at X, namely f ↦ f' • m.

Instances For
    source
    @[simp]
    theorem PowerSeries.mkDerivation_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsScalarTower R (PowerSeries R) M] (m : M) (f : PowerSeries R) :
    ((mkDerivation R) m) f = derivative f • m
    source
    theorem PowerSeries.mkDerivation_X {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsScalarTower R (PowerSeries R) M] (m : M) :
    ((mkDerivation R) m) X = m
    source
    @[simp]
    theorem PowerSeries.mkDerivation_one {R : Type u_1} [CommRing R] :
    (mkDerivation R) 1 = derivative
    source
    noncomputable def PowerSeries.mkDerivationEquiv (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsScalarTower R (PowerSeries R) M] [IsHausdorff (Ideal.span {X}) M] :
    M ≃ₗ[PowerSeries R] Derivation R (PowerSeries R) M

    For an X-adically Hausdorff R⟦X⟧-module M, PowerSeries.mkDerivation is an R⟦X⟧-linear equivalence between M and the derivations R⟦X⟧ → M, inverse to evaluation at X.

    Instances For
      source
      @[simp]
      theorem PowerSeries.mkDerivationEquiv_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsScalarTower R (PowerSeries R) M] [IsHausdorff (Ideal.span {X}) M] (m : M) :
      (mkDerivationEquiv R M) m = (mkDerivation R) m
      source
      @[simp]
      theorem PowerSeries.mkDerivationEquiv_symm_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module (PowerSeries R) M] [Module R M] [IsScalarTower R (PowerSeries R) M] [IsHausdorff (Ideal.span {X}) M] (D : Derivation R (PowerSeries R) M) :
      (mkDerivationEquiv R M).symm D = D X
      source
      theorem Derivation.eq_smul_derivative {R : Type u_1} [CommRing R] (D : Derivation R (PowerSeries R) (PowerSeries R)) :
      D = D PowerSeries.X • PowerSeries.derivative

      Every derivation of R⟦X⟧ is the multiple D X • d⁄dX of the formal derivative.