The multiplicative valuation of Hahn series

Let Γ be a linearly ordered additive group and R a domain. Mathlib's HahnSeries.addVal is the additive valuation x ↦ ord x = x.orderTop with values in WithTop Γ. This file defines its multiplicative counterpart

HahnSeries.valuation Γ R : Valuation R⟦Γ⟧ Γᵐ⁰,

sending a nonzero series of order g to exp (-g) and 0 to 0. Thus series of large order have small valuation. For Γ = ℤ and a field K of coefficients it takes the same values as Mathlib's valuation on K⸨X⸩, which sends f ≠ 0 to exp (-ord f) (TauCeti.LaurentSeries.valuation_eq_exp_neg_order); for Γ = ℚ it restricts to the valuation of the Puiseux field.

The comparison lemmas translate between the two valuations: v x < exp (-g) exactly when g < ord x, and v x ≤ exp (-g) exactly when g ≤ ord x. These are the form in which balls of the valuation topology are described by orders.

Main definitions

• HahnSeries.valuation Γ R: the multiplicative valuation x ↦ exp (-ord x).

Main results

• HahnSeries.valuation_eq_exp_neg_order: a nonzero series of order g has valuation exp (-g).
• HahnSeries.valuation_lt_exp_neg_iff, HahnSeries.valuation_le_exp_neg_iff: valuation balls are order conditions.
• HahnSeries.valuation_le_valuation_iff: the valuation reverses the order of ord.

noncomputable def HahnSeries.valuation (Γ : Type u_1) (R : Type u_2) [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] : Valuation (HahnSeries Γ R) (WithZero (Multiplicative Γ))

The multiplicative valuation on R⟦Γ⟧, sending a nonzero series of order g to exp (-g) and 0 to 0.

theorem HahnSeries.valuation_eq_exp_neg_order {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (hx : x ≠ 0) : (valuation Γ R) x = WithZero.exp (-x.order)

A nonzero Hahn series of order g has valuation exp (-g).

@[simp]

theorem HahnSeries.valuation_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} : (valuation Γ R) x = 0 ↔ x = 0

The valuation of x vanishes exactly when x = 0.

@[simp]

theorem HahnSeries.valuation_single {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] (g : Γ) {r : R} (hr : r ≠ 0) : (valuation Γ R) ((single g) r) = WithZero.exp (-g)

The monomial r t ^ g, for r ≠ 0, has valuation exp (-g).

theorem HahnSeries.valuation_lt_exp_neg_iff {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (g : Γ) : (valuation Γ R) x < WithZero.exp (-g) ↔ ↑g < x.orderTop

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

theorem HahnSeries.valuation_le_exp_neg_iff {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (g : Γ) : (valuation Γ R) x ≤ WithZero.exp (-g) ↔ ↑g ≤ x.orderTop

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

theorem HahnSeries.valuation_le_valuation_iff {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [IsDomain R] {x y : HahnSeries Γ R} : (valuation Γ R) x ≤ (valuation Γ R) y ↔ y.orderTop ≤ x.orderTop

The valuation reverses the order: v x ≤ v y exactly when ord y ≤ ord x.