Weak approximation at finite and infinite places #
This file proves Artin--Whaples weak approximation for a number field in a finite product that
contains both nonarchimedean and archimedean completions. The finite factors are Mathlib's
HeightOneSpectrum.adicCompletion, and the infinite factors are
NumberField.InfinitePlace.Completion.
The proof first applies Mathlib's weak approximation theorem for inequivalent real absolute
values to the disjoint union of the chosen places. At a finite place, the normalized discrete
valuation is viewed as a real absolute value through Valuation.toRealAbsoluteValue. Distinct
finite places are inequivalent, distinct infinite places are inequivalent, and a finite place is
inequivalent to an infinite one because every algebraic integer has finite absolute value at most
one whereas every infinite place sends 2 to 2.
The resulting approximation inside the number field is then promoted to the actual completions. Density of the field in each individual completion supplies nearby field-valued targets, and a second simultaneous approximation remains inside the prescribed product neighbourhood.
Two consequences for a unit of K are derived from it. Prescribing an approximation target at
each of finitely many finite places and a sign at each real place is one open condition on the
product, so one element of Kˣ meets all of them at once; specializing the finite targets to
elements of prescribed valuation gives independent valuations instead. The archimedean half of the
prescription is not redone here: the target family and the estimate that reads a sign off an
approximation of it are
NumberField.exists_forall_apply_eq_one_and_embedding_of_isReal_eq and
NumberField.mul_pos_of_infinitePlace_sub_lt, shared with the purely archimedean statement
NumberField.exists_ne_zero_forall_isReal_pos.
The conclusions use Kˣ to package the required nonvanishing and make signHom applicable. A
K-valued formulation would instead need an explicit x ≠ 0 condition and sign predicates stated
directly in terms of the real embeddings.
Main results #
GlobalNumberFields.weakApproximation_denseRange: the diagonal image of a number field is dense in every finite product of finite and infinite completions.GlobalNumberFields.denseRange_algebraMap_embedding_of_isReal: the same with each real completion read asℝthrough the embedding of its real place.GlobalNumberFields.exists_fieldUnit_valuation_sub_lt_and_signHom_eq: one field unit ofKapproximates independently prescribed targets at finitely many finite places while realizing a prescribed sign at every real place.GlobalNumberFields.exists_fieldUnit_valuation_eq_and_signHom_eq: the same with prescribed valuations in place of the approximation targets.
References #
The weak approximation theorem is due to E. Artin and G. Whaples, Axiomatic characterization of fields by the product formula for valuations, Bull. Amer. Math. Soc. 51 (1945). The mixed number-field formulation also appears in J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II.
Artin--Whaples weak approximation at mixed places. For finite sets Sₑ of finite
places and Sinf of infinite places, the diagonal image of a number field K is dense in the
product of the corresponding finite and infinite completions.
The finite factors are Mathlib's normalized adic completions and the infinite factors are its
completions of K at InfinitePlace K; in particular, this is not merely approximation inside
copies of K equipped with the place topologies.
Weak approximation at finite and real places. The diagonal image of a number field is
dense in the product of its completions at finitely many finite places and of ℝ at finitely
many real places, embedded through the real embeddings of those places.
Simultaneous approximation in Kˣ #
The two statements below use Kˣ to package the required nonvanishing and make signHom
applicable. A K-valued version would need an explicit x ≠ 0 condition and would state the sign
requirements directly as predicates on the real embeddings.
Simultaneous approximation with prescribed signs. Given a finite set S of finite
places, a target a v and a nonzero radius γ v at each place of S, and a prescribed sign at
every real place, one and the same field unit of K approximates each finite target to within
its own radius and has each prescribed sign.
The finite conditions are independent of one another and of the archimedean ones; this is the
Kˣ-valued form of weakApproximation_denseRange, and it is what a congruence-and-positivity
statement for a modulus is built from.
Independent valuations at finitely many finite places, with prescribed signs. There is a
field unit of K whose valuation at each place of a finite set S is the prescribed one, and whose
sign at each real place is the prescribed one.
The valuations at the places of S are prescribed independently of one another and of the signs,
and WithZero.exp (n v) is an arbitrary nonzero value of v.valuation K, so this produces a field
unit of prescribed order at each prime of a modulus and of prescribed sign at each of its real
places — the form in which an ideal is moved to a representative prime to that modulus.
A field unit which is negative at every real place.
Being negative at a real place is exactly being a nonsquare there, so this supplies, in a single
element of Kˣ, the datum b that a sign prescription reads off at the real places of its
prescribed set. Signs are not the only datum a prescription can impose on a field unit —
exists_fieldUnit_valuation_eq_and_signHom_eq prescribes finite-place valuations as well — but
they are the one datum that a single element of Kˣ realizes at every real place at once.