Documentation

TauCeti.RingTheory.HahnSeries.Derivation

Derivations of Hahn series #

For an additive map w : Γ →+ R, scaling the coefficient of t ^ g by w g is an R-derivation HahnSeries.weightDerivation w of HahnSeries Γ R: exponents add under multiplication, so the additivity w (g + h) = w g + w h is exactly the Leibniz rule. For Γ = ℤ and w the integer cast it is the Euler operator t d/dt on Laurent series.

Over a ℚ-algebra R, the Euler operator with the rational cast as weight, followed by multiplication by t⁻¹, is the derivative d/dt of rational-exponent Hahn series, TauCeti.ratHahnSeriesDerivation R, given by the coefficient rule d/dt (t ^ q) = q t ^ (q - 1). It restricts to the derivative of Puiseux series.

HahnSeries.weightDerivation is an R-derivation for the coefficientwise R-algebra structure HahnSeries.instAlgebra, the only one available for a general Γ. When Γ is an ordered semiring, such as ℤ or ℚ, instance search instead finds the structure inherited from R⟦X⟧ through HahnSeries.powerSeriesAlgebra, which agrees with it only propositionally; the derivative TauCeti.ratHahnSeriesDerivation R is stated for the latter, so that it restricts to K-algebras of rational-exponent series such as the Puiseux field.

Main definitions #

Main results #

source
noncomputable def HahnSeries.weightDerivation {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [CommSemiring R] [IsOrderedCancelAddMonoid Γ] (w : Γ →+ R) :
Derivation R (HahnSeries Γ R) (HahnSeries Γ R)

The weight derivation of Hahn series attached to an additive map w : Γ →+ R: it scales the coefficient of t ^ g by w g. For Γ = ℤ and the integer cast this is the Euler operator t d/dt.

Instances For
    source
    @[simp]
    theorem HahnSeries.coeff_weightDerivation {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [CommSemiring R] [IsOrderedCancelAddMonoid Γ] (w : Γ →+ R) (x : HahnSeries Γ R) (g : Γ) :
    ((weightDerivation w) x).coeff g = w g * x.coeff g

    The coefficient of t ^ g in weightDerivation w x is w g times that of x.

    source
    theorem HahnSeries.support_weightDerivation_subset {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [CommSemiring R] [IsOrderedCancelAddMonoid Γ] (w : Γ →+ R) (x : HahnSeries Γ R) :
    ((weightDerivation w) x).support ⊆ x.support

    The support of weightDerivation w x is contained in that of x.

    source
    @[simp]
    theorem HahnSeries.weightDerivation_single {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [PartialOrder Γ] [CommSemiring R] [IsOrderedCancelAddMonoid Γ] (w : Γ →+ R) (g : Γ) (r : R) :
    (weightDerivation w) ((single g) r) = (single g) (w g * r)

    The weight derivation sends the monomial r t ^ g to w g r t ^ g.

    source
    noncomputable def TauCeti.ratHahnSeriesDerivation (R : Type u_1) [CommRing R] [Algebra ℚ R] :
    Derivation R (HahnSeries ℚ R) (HahnSeries ℚ R)

    The derivative d/dt of Hahn series with rational exponents over a ℚ-algebra R, given by d/dt (t ^ q) = q t ^ (q - 1). It is t⁻¹ times the weight derivation for the rational cast, the Euler operator t d/dt.

    It is a derivation for the default R-algebra structure on HahnSeries ℚ R, the one inherited from R⟦X⟧ through HahnSeries.powerSeriesAlgebra, which is only propositionally equal to the coefficientwise structure for which HahnSeries.weightDerivation is stated.

    Instances For
      source
      @[simp]
      theorem TauCeti.coeff_ratHahnSeriesDerivation {R : Type u_1} [CommRing R] [Algebra ℚ R] (x : HahnSeries ℚ R) (q : ℚ) :
      ((ratHahnSeriesDerivation R) x).coeff q = (q + 1) • x.coeff (q + 1)

      The coefficient of t ^ q in the derivative of x is q + 1 times the coefficient of t ^ (q + 1) in x.

      source
      theorem TauCeti.coeff_ratHahnSeriesDerivation_sub_one {R : Type u_1} [CommRing R] [Algebra ℚ R] (x : HahnSeries ℚ R) (q : ℚ) :
      ((ratHahnSeriesDerivation R) x).coeff (q - 1) = q • x.coeff q

      The coefficient of t ^ (q - 1) in the derivative of x is q times the coefficient of t ^ q in x.

      source
      @[simp]
      theorem TauCeti.ratHahnSeriesDerivation_single {R : Type u_1} [CommRing R] [Algebra ℚ R] (q : ℚ) (r : R) :
      (ratHahnSeriesDerivation R) ((HahnSeries.single q) r) = (HahnSeries.single (q - 1)) (q • r)

      Power rule: the derivative of r t ^ q is q r t ^ (q - 1).

      source
      theorem TauCeti.orderTop_le_orderTop_ratHahnSeriesDerivation_add_one {R : Type u_1} [CommRing R] [Algebra ℚ R] (x : HahnSeries ℚ R) :
      x.orderTop ≤ ((ratHahnSeriesDerivation R) x).orderTop + 1

      Differentiation lowers the order by at most one: ord x ≤ ord (dx/dt) + 1.

      source
      theorem TauCeti.ratHahnSeriesDerivation_eq_zero_iff {R : Type u_1} [CommRing R] [Algebra ℚ R] {x : HahnSeries ℚ R} :
      (ratHahnSeriesDerivation R) x = 0 ↔ ∃ (r : R), (algebraMap R (HahnSeries ℚ R)) r = x

      The kernel of d/dt: the rational-exponent Hahn series with derivative zero are the constants.