Weak approximation for discrete valuations

This file proves weak approximation for a finite family of pairwise inequivalent ℤᵐ⁰-valued valuations. It first sends such a valuation through the strictly monotone embedding ℤᵐ⁰ → ℝ≥0 → ℝ, obtaining a real absolute value with exactly the same comparisons. Mathlib's abstract weak approximation theorem for real absolute values then supplies simultaneous open-ball approximation. For normalized valuations, shifting each target by an element of prescribed value gives the equality form with arbitrary integer orders.

The results below are the finite-family approximation engine for abstract ℤᵐ⁰-valued valuations: they mention neither function fields nor places. Weak approximation for places of an algebraic function field — Stichtenoth, Algebraic Function Fields and Codes, second edition, Theorem 1.3.1 — follows from Valuation.exists_forall_sub_eq_exp once the place API supplies the normalized valuation of a place and the inequivalence of distinct normalized places. The proof consumes Mathlib's AbsoluteValue.denseRange_algebraMap_pi rather than rebuilding the Artin--Whaples approximation argument.

Main results

• Valuation.toRealAbsoluteValue realizes a ℤᵐ⁰-valued valuation as a real absolute value.
• Valuation.exists_forall_sub_lt gives simultaneous open-ball approximation.
• Valuation.exists_forall_sub_eq_exp gives prescribed integer orders for normalized valuations.

noncomputable def Valuation.toRealAbsoluteValue {K : Type u_1} [DivisionRing K] (v : Valuation K (WithZero (Multiplicative ℤ))) : AbsoluteValue K ℝ

A ℤᵐ⁰-valued valuation, viewed as a real absolute value through the base-two embedding of its value group. This changes neither comparisons nor equivalence of valuations.

A division ring is needed already here: an AbsoluteValue vanishes only at 0, whereas a valuation on a general ring may have nontrivial support.

Equations

• v.toRealAbsoluteValue = v.toAbsoluteValue Valuation.withZeroMulIntToReal✝ ⋯ Valuation.toRealAbsoluteValue._proof_5✝

@[simp]

theorem Valuation.toRealAbsoluteValue_apply {K : Type u_1} [DivisionRing K] (v : Valuation K (WithZero (Multiplicative ℤ))) (x : K) : v.toRealAbsoluteValue x = ↑((WithZeroMulInt.toNNReal toRealAbsoluteValue_apply._proof_1) (v x))

theorem Valuation.toRealAbsoluteValue_le_iff {K : Type u_1} [DivisionRing K] (v : Valuation K (WithZero (Multiplicative ℤ))) {x y : K} : v.toRealAbsoluteValue x ≤ v.toRealAbsoluteValue y ↔ v x ≤ v y

Passing a discrete valuation to its real absolute value preserves and reflects inequalities.

@[simp]

theorem Valuation.toRealAbsoluteValue_isEquiv_iff {K : Type u_1} [DivisionRing K] (v w : Valuation K (WithZero (Multiplicative ℤ))) : v.toRealAbsoluteValue.IsEquiv w.toRealAbsoluteValue ↔ v.IsEquiv w

Passing discrete valuations to real absolute values preserves and reflects equivalence.

@[simp]

theorem Valuation.toRealAbsoluteValue_isNontrivial_iff {K : Type u_1} [DivisionRing K] (v : Valuation K (WithZero (Multiplicative ℤ))) : v.toRealAbsoluteValue.IsNontrivial ↔ v.IsNontrivial

A discrete valuation is nontrivial exactly when its associated real absolute value is.

theorem Valuation.exists_forall_sub_lt {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (v : ι → Valuation K (WithZero (Multiplicative ℤ))) (h_nontrivial : ∀ (i : ι), (v i).IsNontrivial) (h_inequiv : Pairwise fun (i j : ι) => ¬(v i).IsEquiv (v j)) (a : ι → K) (ε : ι → WithZero (Multiplicative ℤ)) (hε : ∀ (i : ι), ε i ≠ 0) : ∃ (x : K), ∀ (i : ι), (v i) (x - a i) < ε i

Weak approximation for finitely many nontrivial, pairwise inequivalent discrete valuations, in open-ball form.

theorem Valuation.exists_forall_sub_eq_exp {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (v : ι → Valuation K (WithZero (Multiplicative ℤ))) (h_surjective : ∀ (i : ι), Function.Surjective ⇑(v i)) (h_inequiv : Pairwise fun (i j : ι) => ¬(v i).IsEquiv (v j)) (a : ι → K) (r : ι → ℤ) : ∃ (x : K), ∀ (i : ι), (v i) (x - a i) = WithZero.exp (-r i)

Equality-form weak approximation for finitely many normalized discrete valuations. The error at index i has the prescribed valuation exp (-r i), hence the prescribed additive order r i.