The algebra action, the product rule, and residues of φⁿ dφ for Laurent series

For an R-algebra A, the R-algebra structure on A⸨X⸩ is the one inherited from A⟦X⟧ through HahnSeries.ofPowerSeries, so its scalar action is multiplication by the image of a constant power series. This is propositionally, but not definitionally, equal to the coefficientwise action HahnSeries.instSMul found by default.

The scalar tower S → A⟦X⟧ → A⸨X⸩ for any commutative semiring S over which A⟦X⟧ is an algebra (in particular S = R and S = A[X]) is imported from TauCeti.RingTheory.HahnSeries.PowerSeries; the tower over R is what fraction-field constructions such as IsFractionRing.algEquivOfAlgEquiv require to extend an R-algebra equivalence with A⟦X⟧ to one with A⸨X⸩. This file shows that the algebra action of R on A⸨X⸩ agrees with the coefficientwise action, and records that, over a field K, a nonzero Laurent series f ∈ K⸨X⸩ has valuation exp (-ord f), since its power series part is a unit of K⟦X⟧. Consequently a field embedding K → L, applied to every coefficient, preserves valuations.

The second part proves the product rule for the derivative of Laurent series, (f * g)' = f' * g + f * g'. Mathlib defines LaurentSeries.derivative only as a linear map, the first Hasse derivative; the product rule is what makes it a derivation, so that composing it with a ring homomorphism into R⸨X⸩ gives a derivation, as for Laurent expansions of functions. It is reduced to the product rule for power series by writing a Laurent series as a monomial times a power series.

The third part computes the residue of the formal one-form φ ^ n * φ' dX for any power series φ over a field and every integer n: it is (φ.order.toNat : k) for n = -1 and 0 otherwise. For n ≠ -1 in characteristic zero, φ ^ n * φ' is the derivative of φ ^ (n + 1) / (n + 1); in characteristic p this fails when p ∣ n + 1, and the proof uses PowerSeries.nsmul_coeff_mul_succ_pow_succ_eq_coeff_X_mul_pow_mul_derivative instead. By linearity this extends to every Laurent series: a substitution X ↦ φ multiplies the residue of f(X) dX by φ.order.toNat, and in particular preserves the residue when φ.order = 1. Writing a nonzero Laurent series as X ^ (ord f) times a unit power series shows that the residue of the logarithmic derivative f' / f is the order of f.

Main results

• TauCeti.LaurentSeries.coeff_algebraMap_mul: multiplication by a constant of the algebra structure acts coefficientwise.
• TauCeti.LaurentSeries.mem_range_ofPowerSeries_iff: the Laurent series coming from power series are those with no negative exponents.
• TauCeti.laurentSeries_algebraMap_mul_eq_smul: the algebra action agrees with the coefficientwise scalar action, and TauCeti.laurentSeries_isScalarTower_algebra transfers scalar towers from the coefficientwise action to the algebra action.
• TauCeti.LaurentSeries.valuation_eq_exp_neg_order: a nonzero Laurent series f has valuation exp (-ord f); TauCeti.LaurentSeries.valuation_coe gives the same for a nonzero power series.
• TauCeti.LaurentSeries.valuation_mapRingHom: applying a field embedding to the coefficients preserves the valuation.
• PowerSeries.order_coe, PowerSeries.orderTop_coe and PowerSeries.orderTop_coe_of_ne_zero: the order of a power series in R⸨X⸩ agrees with its power series order.
• LaurentSeries.derivative_mul: the product rule for the derivative of Laurent series.
• PowerSeries.coe_derivative and PowerSeries.coe_hasseDeriv: the derivative and the Hasse derivatives of Laurent series extend those of power series.
• LaurentSeries.valuation_derivative_sub_zsmul_single_mul_le: if f vanishes to order at least m, so does f' - m X⁻¹ f.
• LaurentSeries.valuation_le_one_iff: a Laurent series is integral exactly when it has no negative exponents.
• PowerSeries.coeff_neg_one_coe_zpow_mul_derivative_eq_ite and PowerSeries.coeff_neg_one_coe_zpow_mul_derivative: the residue of φ ^ n * φ' for a power series φ is φ.order.toNat if n = -1 and 0 otherwise (in particular 1 vs 0 when φ.order = 1).
• LaurentSeries.coeff_neg_one_map_mul_derivative_eq_nsmul and LaurentSeries.coeff_neg_one_map_mul_derivative: for a substitution X ↦ φ, the residue of f(φ) φ' is φ.order.toNat • f.coeff (-1) (and f.coeff (-1) when φ.order = 1).
• LaurentSeries.coeff_neg_one_derivative_mul_inv: the residue of f' / f is the order of f.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.2, Proposition 4.2.9.

theorem PowerSeries.orderTop_coe_of_ne_zero {R : Type u_1} [Semiring R] {f : PowerSeries R} (hf : f ≠ 0) : ((HahnSeries.ofPowerSeries ℤ R) f).orderTop = ↑↑f.order.toNat

The WithTop ℤ-valued order of a nonzero power series coerced to R⸨X⸩ is (f.order.toNat : ℤ).

@[simp]

theorem PowerSeries.orderTop_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) : ((HahnSeries.ofPowerSeries ℤ R) f).orderTop = ENat.map Nat.cast f.order

The WithTop ℤ-valued order of a power series coerced to R⸨X⸩ is its order, read in WithTop ℤ; both are ⊤ exactly for the zero series.

@[simp]

theorem PowerSeries.order_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) : ((HahnSeries.ofPowerSeries ℤ R) f).order = ↑f.order.toNat

The integer order of a power series coerced to R⸨X⸩ is (f.order.toNat : ℤ).

@[simp]

theorem TauCeti.LaurentSeries.coeff_algebraMap_mul {R : Type u_1} [CommSemiring R] (c : R) (f : LaurentSeries R) (n : ℤ) : ((algebraMap R (LaurentSeries R)) c * f).coeff n = c * f.coeff n

Multiplying a Laurent series by a constant of the R-algebra structure on R⸨X⸩ multiplies each coefficient by that constant.

theorem TauCeti.LaurentSeries.mem_range_ofPowerSeries_iff {R : Type u_1} [CommSemiring R] {f : LaurentSeries R} : f ∈ Set.range ⇑(HahnSeries.ofPowerSeries ℤ R) ↔ ∀ n < 0, f.coeff n = 0

A Laurent series is the image of a power series exactly when its coefficients at negative exponents vanish.

theorem TauCeti.LaurentSeries.valuation_coe_of_isUnit {K : Type u_2} [Field K] {h : PowerSeries K} (hh : IsUnit h) : Valued.v ((HahnSeries.ofPowerSeries ℤ K) h) = 1

A unit of K⟦X⟧, that is a power series of nonzero constant coefficient, has valuation one in K⸨X⸩.

theorem TauCeti.LaurentSeries.isUnit_powerSeriesPart {D : Type u_3} [DivisionRing D] {f : LaurentSeries D} (hf : f ≠ 0) : IsUnit f.powerSeriesPart

The power series part of a nonzero Laurent series over a division ring is a unit: its constant coefficient is the leading coefficient.

theorem TauCeti.LaurentSeries.valuation_eq_exp_neg_order {K : Type u_2} [Field K] {f : LaurentSeries K} (hf : f ≠ 0) : Valued.v f = WithZero.exp (-HahnSeries.order f)

A nonzero Laurent series f has valuation exp (-ord f).

theorem TauCeti.LaurentSeries.valuation_coe {K : Type u_2} [Field K] {g : PowerSeries K} (hg : g ≠ 0) : Valued.v ((HahnSeries.ofPowerSeries ℤ K) g) = WithZero.exp (-↑g.order.toNat)

A nonzero power series g has valuation exp (-ord g) in K⸨X⸩.

@[simp]

theorem TauCeti.LaurentSeries.valuation_mapRingHom {K : Type u_2} [Field K] {L : Type u_3} [Field L] (σ : K →+* L) (f : LaurentSeries K) : Valued.v ((HahnSeries.mapRingHom σ) f) = Valued.v f

Applying a field embedding σ : K →+* L to the coefficients preserves the valuation.

theorem TauCeti.laurentSeries_algebraMap_mul_eq_smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (c : R) (f : LaurentSeries A) : (algebraMap R (LaurentSeries A)) c * f = c • f

Multiplication by a constant of the Laurent-series algebra structure agrees with the coefficientwise scalar action, for Laurent series with coefficients in any R-algebra.

instance TauCeti.laurentSeries_isScalarTower_algebra {R : Type u_1} {M : Type u_2} [CommSemiring R] [SMul (LaurentSeries R) M] [SMul R M] [IsScalarTower R (LaurentSeries R) M] : IsScalarTower R (LaurentSeries R) M

A scalar tower R → R⸨X⸩ → M for the coefficientwise action of R on R⸨X⸩, which is the one found by instance search, is also a scalar tower for the algebra action, since the two actions agree. Derivations out of R⸨X⸩ and Kähler differentials of R⸨X⸩ use the algebra action.

@[simp]

theorem PowerSeries.coe_hasseDeriv {R : Type u_1} [Ring R] (k : ℕ) (f : PowerSeries R) : (HahnSeries.ofPowerSeries ℤ R) ((hasseDeriv k) f) = (LaurentSeries.hasseDeriv R k) ((HahnSeries.ofPowerSeries ℤ R) f)

The Hasse derivatives of Laurent series extend the Hasse derivatives of power series.

@[simp]

theorem PowerSeries.coe_derivative {R : Type u_1} [CommRing R] (f : PowerSeries R) : (HahnSeries.ofPowerSeries ℤ R) (derivative f) = (LaurentSeries.derivative R) ((HahnSeries.ofPowerSeries ℤ R) f)

The derivative of Laurent series extends the derivative of power series.

theorem LaurentSeries.derivative_single_mul {R : Type u_1} [Ring R] (m : ℤ) (c : R) (f : LaurentSeries R) : (derivative R) ((HahnSeries.single m) c * f) = (HahnSeries.single (m - 1)) (↑m * c) * f + (HahnSeries.single m) c * (derivative R) f

The product rule for a monomial over any ring: (c X ^ m * f)' = m c X ^ (m - 1) * f + c X ^ m * f'.

theorem LaurentSeries.coeff_derivative_sub_zsmul_single_mul {R : Type u_1} [Ring R] (m n : ℤ) (f : LaurentSeries R) : ((derivative R) f - m • ((HahnSeries.single (-1)) 1 * f)).coeff n = ↑(n + 1 - m) * f.coeff (n + 1)

The derivative of f agrees with m X⁻¹ f up to a correction whose coefficient of Xⁿ is (n + 1 - m) times the coefficient of Xⁿ⁺¹ in f.

theorem LaurentSeries.derivative_single_mul_coe {R : Type u_1} [CommRing R] (m : ℤ) (c : R) (φ : PowerSeries R) : (derivative R) ((HahnSeries.single m) c * (HahnSeries.ofPowerSeries ℤ R) φ) = (HahnSeries.single (m - 1)) (↑m * c) * (HahnSeries.ofPowerSeries ℤ R) φ + (HahnSeries.single m) c * (HahnSeries.ofPowerSeries ℤ R) (PowerSeries.derivative φ)

The product rule for a monomial times a power series: (c X ^ m * φ)' = m c X ^ (m - 1) * φ + c X ^ m * φ'.

theorem LaurentSeries.derivative_mul {R : Type u_1} [CommRing R] (f g : LaurentSeries R) : (derivative R) (f * g) = (derivative R) f * g + f * (derivative R) g

The product rule for the derivative of Laurent series: (f * g)' = f' * g + f * g'.

theorem LaurentSeries.valuation_derivative_sub_zsmul_single_mul_le {K : Type u_2} [Field K] {m : ℤ} {f : LaurentSeries K} (hf : Valued.v f ≤ WithZero.exp (-m)) : Valued.v ((derivative K) f - m • ((HahnSeries.single (-1)) 1 * f)) ≤ WithZero.exp (-m)

Differentiation lowers the order by at most one, with leading term m X⁻¹ f. If f has valuation at most exp (-m), that is, vanishes to order at least m, then f' - m X⁻¹ f again vanishes to order at least m.

theorem LaurentSeries.valuation_le_one_iff {K : Type u_2} [Field K] {f : LaurentSeries K} : Valued.v f ≤ 1 ↔ ∀ n < 0, f.coeff n = 0

A Laurent series lies in the valuation ring exactly when it has no negative exponents.

theorem PowerSeries.coeff_neg_one_coe_zpow_mul_derivative_eq_ite {k : Type u_1} [Field k] (φ : PowerSeries k) (n : ℤ) : ((HahnSeries.ofPowerSeries ℤ k) φ ^ n * (LaurentSeries.derivative k) ((HahnSeries.ofPowerSeries ℤ k) φ)).coeff (-1) = if n = -1 then ↑φ.order.toNat else 0

The residue of φ ^ n dφ for a power series φ of arbitrary order. Over a field k, for any power series φ : k⟦X⟧ and integer n : ℤ, the coefficient of X⁻¹ in φ ^ n * φ' is (φ.order.toNat : k) if n = -1 and 0 otherwise.

theorem PowerSeries.coeff_neg_one_coe_zpow_mul_derivative {k : Type u_1} [Field k] {φ : PowerSeries k} (hφ : φ.order = 1) (n : ℤ) : ((HahnSeries.ofPowerSeries ℤ k) φ ^ n * (LaurentSeries.derivative k) ((HahnSeries.ofPowerSeries ℤ k) φ)).coeff (-1) = if n = -1 then 1 else 0

The residue of φ ^ n dφ. For a power series φ of order one over a field, the coefficient of X⁻¹ in the Laurent series φ ^ n * φ' is 1 if n = -1 and 0 otherwise. Equivalently, the residue of X ^ n dX is unchanged by the substitution X ↦ φ.

theorem LaurentSeries.coeff_neg_one_derivative_mul_inv {K : Type u_1} [Field K] (f : LaurentSeries K) : ((derivative K) f * f⁻¹).coeff (-1) = ↑(HahnSeries.order f)

The residue of a logarithmic derivative is the order. Over a field, the coefficient of X⁻¹ in f' / f is the order of f.

theorem LaurentSeries.coeff_neg_one_map_mul_derivative_eq_nsmul {K : Type u_1} [Field K] (ψ : LaurentSeries K →+* LaurentSeries K) (hC : ∀ (c : K), ψ (HahnSeries.C c) = HahnSeries.C c) (hψ : ∀ (f : LaurentSeries K), Valued.v f ≤ 1 → Valued.v (ψ f) ≤ 1) {φ : PowerSeries K} (hX : ψ ((HahnSeries.single 1) 1) = (HahnSeries.ofPowerSeries ℤ K) φ) (f : LaurentSeries K) : (ψ f * (derivative K) ((HahnSeries.ofPowerSeries ℤ K) φ)).coeff (-1) = φ.order.toNat • f.coeff (-1)

The residue under a general-order substitution. Let ψ be a ring endomorphism of K⸨X⸩ fixing the constants, sending power series to power series, and sending X to a power series φ, such as the substitution X ↦ φ. Then the coefficient of X⁻¹ in ψ f * φ' is φ.order.toNat times the coefficient of X⁻¹ in f.

theorem LaurentSeries.coeff_neg_one_map_mul_derivative {K : Type u_1} [Field K] (ψ : LaurentSeries K →+* LaurentSeries K) (hC : ∀ (c : K), ψ (HahnSeries.C c) = HahnSeries.C c) (hψ : ∀ (f : LaurentSeries K), Valued.v f ≤ 1 → Valued.v (ψ f) ≤ 1) {φ : PowerSeries K} (hφ : φ.order = 1) (hX : ψ ((HahnSeries.single 1) 1) = (HahnSeries.ofPowerSeries ℤ K) φ) (f : LaurentSeries K) : (ψ f * (derivative K) ((HahnSeries.ofPowerSeries ℤ K) φ)).coeff (-1) = f.coeff (-1)

Residues are invariant under a coordinate-change substitution (ord φ = 1). Let ψ be a ring endomorphism of K⸨X⸩ fixing the constants, sending power series to power series, and sending X to a power series φ of order one, such as the substitution X ↦ φ. Then the coefficient of X⁻¹ in ψ f * φ' is the coefficient of X⁻¹ in f: the residue of f(X) dX equals that of f(φ) dφ.