Documentation

TauCeti.RingTheory.LaurentSeries.Rescale

Rescaling formal Laurent series #

For a unit a of a commutative semiring R, the substitution f (X) ↦ f (a X) is an R-algebra automorphism of R⸨X⸩. It multiplies the coefficient of Xⁿ by the unit a ^ n, for every integer n, and extends PowerSeries.rescale on power series.

The construction is the twist HahnSeries.twistEquiv by the character n ↦ a ^ n. This makes rescaling available without a fraction field or a field of coefficients.

Rescaling an expanded series f (X ^ d) by a is expansion of the series rescaled by a ^ d. Consequently, rescaling by a d-th root of unity fixes every expanded series.

Main definitions #

Main results #

source
noncomputable def TauCeti.LaurentSeries.rescale {R : Type u_1} [CommSemiring R] :
Rˣ →* LaurentSeries R ≃ₐ[R] LaurentSeries R

The rescaling f (X) ↦ f (a X) of Laurent series by a unit a, as an R-algebra automorphism. It multiplies the coefficient of Xⁿ by a ^ n, and the automorphisms for a and b compose to the one for a * b.

Instances For
    source
    @[simp]
    theorem TauCeti.LaurentSeries.coeff_rescale {R : Type u_1} [CommSemiring R] (a : Rˣ) (f : LaurentSeries R) (n : ℤ) :
    ((rescale a) f).coeff n = ↑(a ^ n) * f.coeff n

    Rescaling by a multiplies the coefficient of Xⁿ by a ^ n.

    source
    @[simp]
    theorem TauCeti.LaurentSeries.rescale_single {R : Type u_1} [CommSemiring R] (a : Rˣ) (n : ℤ) (c : R) :
    (rescale a) ((HahnSeries.single n) c) = (HahnSeries.single n) (↑(a ^ n) * c)

    Rescaling sends the monomial c Xⁿ to a ^ n c Xⁿ.

    source
    @[simp]
    theorem TauCeti.LaurentSeries.rescale_coe {R : Type u_1} [CommSemiring R] (a : Rˣ) (f : PowerSeries R) :
    (rescale a) ((HahnSeries.ofPowerSeries ℤ R) f) = (HahnSeries.ofPowerSeries ℤ R) ((PowerSeries.rescale ↑a) f)

    On power series, rescaling Laurent series is PowerSeries.rescale.

    source
    theorem TauCeti.LaurentSeries.rescale_expand {R : Type u_1} [CommSemiring R] (a : Rˣ) (d : ℕ+) (f : LaurentSeries R) :
    (rescale a) ((LaurentSeries.expand R d) f) = (LaurentSeries.expand R d) ((rescale (a ^ ↑d)) f)

    Rescaling an expanded series by a is expanding the series rescaled by a ^ d: f ((a X) ^ d) = (f (a ^ d X)) (X ^ d).

    source
    theorem TauCeti.LaurentSeries.rescale_expand_of_pow_eq_one {R : Type u_1} [CommSemiring R] {a : Rˣ} {d : ℕ+} (ha : a ^ ↑d = 1) (f : LaurentSeries R) :
    (rescale a) ((LaurentSeries.expand R d) f) = (LaurentSeries.expand R d) f

    Rescaling by a d-th root of unity fixes every series expanded by X ↦ X ^ d.

    source
    @[simp]
    theorem TauCeti.LaurentSeries.valuation_rescale {K : Type u_2} [Field K] (a : Kˣ) (f : LaurentSeries K) :
    Valued.v ((rescale a) f) = Valued.v f

    Rescaling by a unit preserves the Laurent valuation: it does not change which coefficients vanish.