Convergence of formal Laurent series

This file characterizes convergence in the valuation topology on a Laurent-series field. A family converges precisely when its supports are eventually bounded below by one common integer and each coefficient eventually agrees with the corresponding coefficient of the limit. Equivalently, the order of the difference eventually exceeds every prescribed integer.

The common lower bound is essential. The monomials X⁻¹, X⁻², ... have every fixed coefficient eventually equal to zero, but they do not converge to zero in the valuation topology.

The order formulation is the form used to prove continuity of operations on Laurent series: a map is continuous once every prescribed order of the output difference is reached from some order of the input difference. The coefficient formulation instead identifies limits concretely, coefficient by coefficient, once a common lower bound on the supports is known.

The reverse implication in the coefficient criterion adapts LaurentSeries.Cauchy.eventually_mem_nhds from Mathlib: its coefficient agreement for a Cauchy limit is replaced here by the assumed pointwise agreement with the prescribed limit.

Main results

• TauCeti.tendsto_laurentSeries_iff_coeff characterizes convergence by a common lower support bound and eventual equality of every coefficient.
• TauCeti.tendsto_laurentSeries_iff_orderTop_sub gives the equivalent order formulation.
• TauCeti.LaurentSeries.continuous_mapRingHom: applying a field embedding to the coefficients is continuous.
• TauCeti.laurentSeries_eventually_coeff_single_neg_succ_eq_zero and TauCeti.laurentSeries_not_tendsto_single_neg_succ exhibit the coefficientwise counterexample.

theorem TauCeti.tendsto_laurentSeries_iff_coeff {K : Type u_1} [Field K] {ι : Type u_2} {l : Filter ι} (f : ι → LaurentSeries K) (g : LaurentSeries K) : Filter.Tendsto f l (nhds g) ↔ (∃ (b : ℤ), ∀ᶠ (i : ι) in l, ∀ z < b, (f i).coeff z = 0) ∧ ∀ (z : ℤ), ∀ᶠ (i : ι) in l, (f i).coeff z = g.coeff z

A family of Laurent series converges exactly when its supports have an eventual common lower bound and each coefficient eventually agrees with the corresponding coefficient of the limit.

The statement applies to arbitrary filters, not only sequences; for the bottom filter both sides hold automatically. No topology on the coefficient field is used: coefficient stabilization is literal eventual equality.

theorem TauCeti.tendsto_laurentSeries_iff_orderTop_sub {K : Type u_1} [Field K] {ι : Type u_2} {l : Filter ι} (f : ι → LaurentSeries K) (g : LaurentSeries K) : Filter.Tendsto f l (nhds g) ↔ ∀ (D : ℤ), ∀ᶠ (i : ι) in l, ↑D ≤ HahnSeries.orderTop (f i - g)

Convergence of Laurent series is equivalent to the order of the difference eventually being at least every prescribed integer. This includes a zero difference, whose order is ⊤.

theorem TauCeti.LaurentSeries.continuous_mapRingHom {K : Type u_1} [Field K] {L : Type u_2} [Field L] (σ : K →+* L) : Continuous ⇑(HahnSeries.mapRingHom σ)

Applying a field embedding σ : K →+* L to the coefficients is continuous for the valuation topologies, since it preserves orders.

theorem TauCeti.laurentSeries_eventually_coeff_single_neg_succ_eq_zero {R : Type u_2} [Zero R] (r : R) (z : ℤ) : ∀ᶠ (n : ℕ) in Filter.atTop, ((HahnSeries.single (-↑(n + 1))) r).coeff z = 0

Every fixed coefficient of the sequence of monomials with exponents -1, -2, ... and fixed coefficient r is eventually zero.

theorem TauCeti.laurentSeries_not_tendsto_single_neg_succ {K : Type u_1} [Field K] : ¬Filter.Tendsto (fun (n : ℕ) => (HahnSeries.single (-↑(n + 1))) 1) Filter.atTop (nhds 0)

The sequence X⁻¹, X⁻², ... does not converge to zero in the Laurent valuation topology, despite the eventual vanishing of each fixed coefficient.