Differentiation of Laurent series

This file bundles the coefficientwise formal derivative D of Laurent series as a derivation over any commutative ring, using the Leibniz rule from LaurentSeries.Basic. The bundle allows the universal property of Kähler differentials to compare it with differentiation of algebraic functions in a local parameter. Laurent derivations carry the commutator Lie algebra structure over the coefficient ring, with [aD, bD] = (a Db - b Da)D over any commutative ring.

It then records how D interacts with the order ord = HahnSeries.orderTop and with the valuation topology of K⸨X⸩. The coefficient of Xⁿ⁻¹ in D f is n times the coefficient of Xⁿ in f, so D lowers the order by at most one. The order drops by exactly one when the leading exponent r times the leading coefficient is nonzero, for instance over a field in which r is nonzero. In general the order of D f is one less than the first exponent n with n • f.coeff n ≠ 0, and D f = 0 when there is no such exponent. Without additive torsion, as in characteristic zero, the kernel of D is the constants. Over a field, D satisfies the inverse and quotient rules, and it maps the neighbourhood {f | v f ≤ exp (-m)} of zero into {f | v f ≤ exp (-(m - 1))}, so it is continuous for the valuation topology.

The underlying linear map is Mathlib's LaurentSeries.derivative; no new differentiation operation is introduced.

Main results

• TauCeti.laurentSeriesDerivation: D as a derivation.
• Derivation.laurentSeriesLieRing and Derivation.laurentSeriesLieAlgebra: the commutator Lie structures on Laurent derivations.
• LaurentSeries.lie_smul_laurentSeriesDerivation: the coefficient formula for the commutator.
• LaurentSeries.weightDerivation_intCastAddHom: the weight derivation of the integer cast is the Euler operator X D.
• LaurentSeries.coeff_derivative_order_sub_one: the coefficient of X ^ (r - 1) in D f is r times the leading coefficient of f, where r = f.order.
• LaurentSeries.orderTop_le_orderTop_derivative_add_one: ord f ≤ ord (D f) + 1.
• LaurentSeries.zero_le_orderTop_derivative: D maps power series to power series.
• LaurentSeries.zero_le_orderTop_mul_derivative: if f and g are power series, so is f D g.
• LaurentSeries.orderTop_derivative_eq_sub_one: the order of D f is one less than the first exponent whose coefficient survives differentiation.
• LaurentSeries.orderTop_derivative_eq_order_sub_one_of_cast_ne_zero: if the order r of f is nonzero in a ring without zero divisors, then ord (D f) = r - 1.
• LaurentSeries.derivative_eq_zero_iff_exists_C: without additive torsion the kernel of D consists of the constants.
• LaurentSeries.derivative_inv and LaurentSeries.derivative_div: the inverse and quotient rules over a field.
• LaurentSeries.continuous_derivative: D is continuous for the valuation topology.
• LaurentSeries.ratHahnSeriesDerivation_ramifiedEmbedding: the chain rule on ramified levels. Under the level-n embedding u ↦ t ^ (1 / n) into rational-exponent Hahn series, the derivative d/dt is (1 / n) u ^ (1 - n) D.

noncomputable def TauCeti.laurentSeriesDerivation (R : Type u_1) [CommRing R] : Derivation R (LaurentSeries R) (LaurentSeries R)

Formal Laurent differentiation as a derivation. Its linear map is the existing coefficientwise derivative.

@[simp]

theorem TauCeti.laurentSeriesDerivation_apply (R : Type u_1) [CommRing R] (f : LaurentSeries R) : (laurentSeriesDerivation R) f = (LaurentSeries.derivative R) f

The bundled Laurent derivation evaluates as the coefficientwise derivative.

@[instance_reducible]

noncomputable instance Derivation.laurentSeriesLieRing {R : Type u_1} [CommRing R] : LieRing (Derivation R (LaurentSeries R) (LaurentSeries R))

The commutator Lie ring on Laurent derivations with their coefficientwise codomain scalars. The native derivation Lie ring uses the algebra-induced codomain module; these scalar actions agree. Additive transport keeps the existing additive group on derivations.

theorem Derivation.laurentSeries_commutator_apply {R : Type u_1} [CommRing R] (δ ε : Derivation R (LaurentSeries R) (LaurentSeries R)) (f : LaurentSeries R) : ⁅δ, ε⁆ f = δ (ε f) - ε (δ f)

Evaluation of the commutator through the coefficientwise Laurent scalar presentation.

@[instance_reducible]

noncomputable instance Derivation.laurentSeriesLieAlgebra {R : Type u_1} [CommRing R] : LieAlgebra R (Derivation R (LaurentSeries R) (LaurentSeries R))

Laurent derivations form a Lie algebra over the coefficient ring, retaining the existing coefficientwise scalar action on derivations.

theorem LaurentSeries.lie_smul_laurentSeriesDerivation {R : Type u_1} [CommRing R] (a b : LaurentSeries R) : ⁅a • TauCeti.laurentSeriesDerivation R, b • TauCeti.laurentSeriesDerivation R⁆ = (a * (TauCeti.laurentSeriesDerivation R) b - b * (TauCeti.laurentSeriesDerivation R) a) • TauCeti.laurentSeriesDerivation R

The commutator of Laurent vector fields has coefficient a D b - b D a. This formula uses no characteristic assumption.

theorem LaurentSeries.coeff_derivative {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] (f : LaurentSeries V) (n : ℤ) : ((derivative R) f).coeff n = (n + 1) • f.coeff (n + 1)

The coefficient of Xⁿ in f' is n + 1 times the coefficient of Xⁿ⁺¹ in f.

theorem LaurentSeries.coeff_derivative_sub_one {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] (f : LaurentSeries V) (n : ℤ) : ((derivative R) f).coeff (n - 1) = n • f.coeff n

The coefficient of Xⁿ⁻¹ in f' is n times the coefficient of Xⁿ in f.

theorem LaurentSeries.coeff_neg_one_derivative {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] (f : LaurentSeries V) : ((derivative R) f).coeff (-1) = 0

The residue of a formal derivative is zero, including for module-valued coefficients.

theorem LaurentSeries.coeff_derivative_order_sub_one {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] (f : LaurentSeries V) : ((derivative R) f).coeff (HahnSeries.order f - 1) = HahnSeries.order f • HahnSeries.leadingCoeff f

The coefficient of X ^ (r - 1) in f', where r is the order of f, is r times the leading coefficient of f.

theorem LaurentSeries.orderTop_le_orderTop_derivative_add_one {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] (f : LaurentSeries V) : HahnSeries.orderTop f ≤ HahnSeries.orderTop ((derivative R) f) + 1

Differentiation lowers the order by at most one: ord f ≤ ord f' + 1.

theorem LaurentSeries.zero_le_orderTop_derivative {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] {f : LaurentSeries V} (hf : 0 ≤ HahnSeries.orderTop f) : 0 ≤ HahnSeries.orderTop ((derivative R) f)

Differentiation preserves power series: if f has no negative powers of X, neither has f'.

theorem LaurentSeries.orderTop_derivative_eq_sub_one {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] {f : LaurentSeries V} {n : ℤ} (hn : n • f.coeff n ≠ 0) (hlt : ∀ m < n, m • f.coeff m = 0) : HahnSeries.orderTop ((derivative R) f) = ↑(n - 1)

If n is the first exponent with n • f.coeff n ≠ 0, then f' has order n - 1.

theorem LaurentSeries.orderTop_derivative_eq_order_sub_one {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] {f : LaurentSeries V} (h : HahnSeries.order f • HahnSeries.leadingCoeff f ≠ 0) : HahnSeries.orderTop ((derivative R) f) = ↑(HahnSeries.order f - 1)

If the order r of f times its leading coefficient is nonzero, then f' has order r - 1.

theorem LaurentSeries.derivative_eq_zero_iff {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] {f : LaurentSeries V} : (derivative R) f = 0 ↔ ∀ (n : ℤ), n • f.coeff n = 0

A Laurent series has derivative zero exactly when n • f.coeff n = 0 for every exponent n.

theorem LaurentSeries.derivative_eq_zero_iff_eq_single {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommGroup V] [Module R V] [IsAddTorsionFree V] {f : LaurentSeries V} : (derivative R) f = 0 ↔ f = (HahnSeries.single 0) (f.coeff 0)

Without additive torsion, a Laurent series has derivative zero exactly when it is constant.

theorem LaurentSeries.zero_le_orderTop_mul_derivative {R : Type u_1} [Ring R] {f g : LaurentSeries R} (hf : 0 ≤ HahnSeries.orderTop f) (hg : 0 ≤ HahnSeries.orderTop g) : 0 ≤ HahnSeries.orderTop (f * (derivative R) g)

Vector fields regular at the origin preserve power series: if f and g have no negative powers of X, neither has f g'.

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

The Euler operator X D multiplies the coefficient of Xⁿ by n.

theorem LaurentSeries.weightDerivation_intCastAddHom {R : Type u_1} [CommRing R] (f : LaurentSeries R) : (HahnSeries.weightDerivation (Int.castAddHom R)) f = (HahnSeries.single 1) 1 * (derivative R) f

The weight derivation of the integer cast is the Euler operator X D.

theorem LaurentSeries.orderTop_derivative_eq_order_sub_one_of_cast_ne_zero {R : Type u_1} [Ring R] [NoZeroDivisors R] {f : LaurentSeries R} (h : ↑(HahnSeries.order f) ≠ 0) : HahnSeries.orderTop ((derivative R) f) = ↑(HahnSeries.order f - 1)

If the order r of f is nonzero in a ring R without zero divisors, for instance a field in which r is nonzero, then f' has order r - 1. Nonvanishing of r forces f ≠ 0, because the zero series has order 0.

theorem LaurentSeries.derivative_eq_zero_iff_exists_C {R : Type u_1} [Ring R] [IsAddTorsionFree R] {f : LaurentSeries R} : (derivative R) f = 0 ↔ ∃ (c : R), HahnSeries.C c = f

The kernel of the derivative. Over a ring without additive torsion, for instance a field of characteristic zero, the Laurent series with derivative zero are exactly the constants.

theorem LaurentSeries.ratHahnSeriesDerivation_ramifiedEmbedding {R : Type u_1} [CommRing R] [Algebra ℚ R] (n : ℕ+) (f : LaurentSeries R) : (TauCeti.ratHahnSeriesDerivation R) ((ramifiedEmbedding R n) f) = (ramifiedEmbedding R n) ((HahnSeries.single (1 - ↑↑n)) ((algebraMap ℚ R) (↑↑n)⁻¹) * (derivative R) f)

Chain rule on ramified levels: under the level-n embedding u ↦ t ^ (1 / n), the derivative d/dt of rational-exponent Hahn series is (1 / n) u ^ (1 - n) d/du.

theorem LaurentSeries.derivative_inv {K : Type u_1} [Field K] (f : LaurentSeries K) : (derivative K) f⁻¹ = -(f⁻¹ ^ 2 * (derivative K) f)

The inverse rule: (f⁻¹)' = -(f⁻¹ ^ 2 * f').

theorem LaurentSeries.derivative_div {K : Type u_1} [Field K] (f g : LaurentSeries K) : (derivative K) (f / g) = ((derivative K) f * g - f * (derivative K) g) / g ^ 2

The quotient rule: (f / g)' = (f' * g - f * g') / g ^ 2.

theorem LaurentSeries.valuation_derivative_le {K : Type u_1} [Field K] {m : ℤ} {f : LaurentSeries K} (hf : Valued.v f ≤ WithZero.exp (-m)) : Valued.v ((derivative K) f) ≤ WithZero.exp (-(m - 1))

If f vanishes to order at least m, then f' vanishes to order at least m - 1.

theorem LaurentSeries.continuous_derivative {K : Type u_1} [Field K] : Continuous ⇑(derivative K)

The derivative of Laurent series is continuous for the valuation topology.