Weak approximation at finitely many finite places

Proved

NumberField.denseRange_algebraMap_pi_adicCompletion

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorylocal-fieldsnumber-theory

Let $K$ be a number field and let $S$ be a finite set of pairwise distinct finite places of $K$ (nonzero prime ideals $w$ of $\mathcal O_K$ ), with $K_w$ the $w$ -adic completion. Then the diagonal embedding

K \longrightarrow \prod_{w \in S} K_w, \qquad x \longmapsto (x)_{w \in S},

has dense image (for the product topology).

Equivalently: given $x_w \in K_w$ for $w \in S$ and $\varepsilon > 0$ , there is $x \in K$ with $|x - x_w|_w < \varepsilon$ for all $w \in S$ . This is the non-archimedean case of the Artin–Whaples approximation theorem; Mathlib already contains the archimedean analogue NumberField.InfinitePlace.denseRange_algebraMap_pi.

Formalization Note $S$ is a Finset of HeightOneSpectrum (𝓞 K); the product is indexed by the elements of $S$ .

Preamble

import Mathlib

open NumberField IsDedekindDomain
open scoped TensorProduct

Formal statement

namespace NumberField

theorem denseRange_algebraMap_pi_adicCompletion {K : Type*} [Field K] [NumberField K] (S : Finset (HeightOneSpectrum (𝓞 K))) :
    DenseRange (fun x : K => fun w : S =>
      algebraMap K ((w : HeightOneSpectrum (𝓞 K)).adicCompletion K) x) := by sorry

end NumberField

Source

J. Neukirch, Algebraic Number Theory, Grundlehren der math. Wiss. 322, Springer 1999, Chapter II, §3, Approximation Theorem (3.4) (case of finitely many inequivalent non-archimedean valuations of

K

View graph