The valuation and topology of the Puiseux field

The Puiseux field puiseuxField K ⊆ HahnSeries ℚ K inherits from the rational Hahn series the additive valuation ord = orderTop with values in WithTop ℚ, and the multiplicative valuation exp (-ord) with values in ℚᵐ⁰. This file restricts both to the Puiseux field and gives it the resulting valuation topology, through a Valued instance.

On the level-n copy of K⸨X⸩, embedded by X ↦ t ^ (1 / n), the Puiseux order is the integer order of the Laurent series divided by n. Consequently each level embedding is a topological embedding, that is, a homeomorphism onto its image. Neighbourhoods of zero are described by orders: {x | q ≤ ord x} for q ∈ ℚ form a basis, and a family converges to x exactly when the order of its difference with x eventually exceeds every rational bound.

Unlike each level, the Puiseux field is not complete. The partial sums of ∑ j, t ^ ((j + 1) + 1 / (j + 2)) form a Cauchy sequence, since the orders of the terms tend to infinity. A limit would have every monomial of this series in its support, by comparing coefficients, but the denominators j + 2 of these exponents are unbounded, so no Puiseux series has them all in its support.

Main definitions

• TauCeti.puiseuxField.addVal K: the additive valuation ord on the Puiseux field.
• TauCeti.puiseuxField.valuation K: the multiplicative valuation exp (-ord), which defines the Valued instance on puiseuxField K.

Main results

• TauCeti.puiseuxField.addVal_levelEmbedding: on level n, the order is the integer order divided by n.
• TauCeti.puiseuxField.hasBasis_nhds_zero: the order balls form a basis of neighbourhoods of zero, and TauCeti.puiseuxField.tendsto_iff_addVal_sub is the resulting convergence criterion.
• TauCeti.puiseuxField.isEmbedding_levelEmbedding: every level embedding is a topological embedding.
• TauCeti.puiseuxField.cauchySeq_sum_single: partial sums of monomials with exponents tending to infinity are Cauchy.
• TauCeti.puiseuxField.not_tendsto_sum_single: such partial sums have no limit when the denominators of the exponents are unbounded.
• TauCeti.puiseuxField.not_completeSpace: the Puiseux field is not complete.

The valuations

noncomputable def TauCeti.puiseuxField.addVal (K : Type u_1) [Field K] : AddValuation (↥(puiseuxField K)) (WithTop ℚ)

The additive valuation ord = orderTop on the Puiseux field, with values in WithTop ℚ.

noncomputable def TauCeti.puiseuxField.valuation (K : Type u_1) [Field K] : Valuation (↥(puiseuxField K)) (WithZero (Multiplicative ℚ))

The multiplicative valuation on the Puiseux field, sending a nonzero series of order q to exp (-q).

@[instance_reducible]

noncomputable instance TauCeti.puiseuxField.instValuedSubtypeHahnSeriesRatMemIntermediateFieldWithZeroMultiplicative (K : Type u_1) [Field K] : Valued (↥(puiseuxField K)) (WithZero (Multiplicative ℚ))

The Puiseux field carries the valuation topology of TauCeti.puiseuxField.valuation.

@[simp]

theorem TauCeti.puiseuxField.addVal_apply {K : Type u_1} [Field K] (x : ↥(puiseuxField K)) : (addVal K) x = (↑x).orderTop

The additive valuation of a Puiseux series is its order as a rational Hahn series.

@[simp]

theorem TauCeti.puiseuxField.valuation_apply {K : Type u_1} [Field K] (x : ↥(puiseuxField K)) : (valuation K) x = (HahnSeries.valuation ℚ K) ↑x

The multiplicative valuation of a Puiseux series is its valuation as a rational Hahn series.

@[simp]

theorem TauCeti.puiseuxField.v_eq_valuation {K : Type u_1} [Field K] : Valued.v = valuation K

The valuation of the Valued instance is TauCeti.puiseuxField.valuation.

theorem TauCeti.puiseuxField.valuation_lt_exp_neg_iff {K : Type u_1} [Field K] (q : ℚ) {x : ↥(puiseuxField K)} : (valuation K) x < WithZero.exp (-q) ↔ ↑q < (addVal K) x

The valuation of x is below exp (-q) exactly when the order of x exceeds q.

theorem TauCeti.puiseuxField.valuation_le_exp_neg_iff {K : Type u_1} [Field K] (q : ℚ) {x : ↥(puiseuxField K)} : (valuation K) x ≤ WithZero.exp (-q) ↔ ↑q ≤ (addVal K) x

The valuation of x is at most exp (-q) exactly when the order of x is at least q.

theorem TauCeti.puiseuxField.addVal_single {K : Type u_1} [Field K] (q : ℚ) {a : K} (ha : a ≠ 0) : (addVal K) (single K q a) = ↑q

The monomial a t ^ q, for a ≠ 0, has order q.

theorem TauCeti.puiseuxField.valuation_single {K : Type u_1} [Field K] (q : ℚ) {a : K} (ha : a ≠ 0) : (valuation K) (single K q a) = WithZero.exp (-q)

The monomial a t ^ q, for a ≠ 0, has valuation exp (-q).

theorem TauCeti.puiseuxField.addVal_levelEmbedding {K : Type u_1} [Field K] (n : ℕ+) (f : LaurentSeries K) : (addVal K) ((levelEmbedding K n) f) = WithTop.map (fun (k : ℤ) => ↑k / ↑↑n) (HahnSeries.orderTop f)

On level n, the order of the Puiseux field is the integer order of K⸨X⸩ divided by n.

theorem TauCeti.puiseuxField.valuation_levelEmbedding {K : Type u_1} [Field K] (n : ℕ+) {f : LaurentSeries K} (hf : f ≠ 0) : (valuation K) ((levelEmbedding K n) f) = WithZero.exp (-(↑(HahnSeries.order f) / ↑↑n))

On level n, a nonzero Laurent series of order k has Puiseux valuation exp (-(k / n)).

theorem TauCeti.puiseuxField.div_le_addVal_levelEmbedding_iff {K : Type u_1} [Field K] (n : ℕ+) (f : LaurentSeries K) (k : ℤ) : ↑(↑k / ↑↑n) ≤ (addVal K) ((levelEmbedding K n) f) ↔ ↑k ≤ HahnSeries.orderTop f

On level n, the order bound k / n ≤ ord in the Puiseux field is the integer order bound k ≤ ord in K⸨X⸩.

The valuation topology

theorem TauCeti.puiseuxField.hasBasis_nhds_zero {K : Type u_1} [Field K] : (nhds 0).HasBasis (fun (x : ℚ) => True) fun (q : ℚ) => {x : ↥(puiseuxField K) | ↑q ≤ (addVal K) x}

The order balls {x | q ≤ ord x}, for q ∈ ℚ, form a basis of neighbourhoods of zero in the Puiseux field.

theorem TauCeti.puiseuxField.tendsto_iff_addVal_sub {K : Type u_1} [Field K] {ι : Type u_2} {l : Filter ι} (f : ι → ↥(puiseuxField K)) (x : ↥(puiseuxField K)) : Filter.Tendsto f l (nhds x) ↔ ∀ (q : ℚ), ∀ᶠ (i : ι) in l, ↑q ≤ (addVal K) (f i - x)

Convergence criterion: a family of Puiseux series converges to x exactly when the order of its difference with x eventually exceeds every rational bound.

theorem TauCeti.puiseuxField.continuous_levelEmbedding {K : Type u_1} [Field K] (n : ℕ+) : Continuous ⇑(levelEmbedding K n)

Every level embedding is continuous.

theorem TauCeti.puiseuxField.isEmbedding_levelEmbedding {K : Type u_1} [Field K] (n : ℕ+) : Topology.IsEmbedding ⇑(levelEmbedding K n)

Every level embedding is a topological embedding: K⸨X⸩ is homeomorphic to its level-n image in the Puiseux field.

Non-completeness

theorem TauCeti.puiseuxField.cauchySeq_sum_single {K : Type u_1} [Field K] {e : ℕ → ℚ} (he : Filter.Tendsto e Filter.atTop Filter.atTop) (c : ℕ → K) : CauchySeq fun (N : ℕ) => ∑ j ∈ Finset.range N, single K (e j) (c j)

Partial sums of monomials whose exponents tend to infinity form a Cauchy sequence.

theorem TauCeti.puiseuxField.not_tendsto_sum_single {K : Type u_1} [Field K] {e : ℕ → ℚ} (he : Function.Injective e) (hden : ∀ (n : ℕ+), ∃ (j : ℕ), ¬(e j).den ∣ ↑n) {c : ℕ → K} (hc : ∀ (j : ℕ), c j ≠ 0) (x : ↥(puiseuxField K)) : ¬Filter.Tendsto (fun (N : ℕ) => ∑ j ∈ Finset.range N, single K (e j) (c j)) Filter.atTop (nhds x)

If the exponents e j are distinct and their denominators are not all divisors of a single positive integer, then partial sums of the monomials c j t ^ (e j), with c j ≠ 0, converge to no Puiseux series: a limit would contain every exponent e j in its support.

theorem TauCeti.puiseuxField.not_completeSpace (K : Type u_1) [Field K] : ¬CompleteSpace ↥(puiseuxField K)

The Puiseux field is not complete. The partial sums of ∑ j, t ^ ((j + 1) + 1 / (j + 2)) form a Cauchy sequence without a limit.