Simultaneous approximation in finitely many adic completions

Let R be a Dedekind domain with fraction field K. Given finitely many height one primes v of R and an element of the ring of integers 𝒪_v of K_v at each of them, a single element of R approximates all of them at once, to any prescribed precision at each place. This combines the single-place density of R in 𝒪_v (HeightOneSpectrum.exists_valued_sub_le) with the Chinese remainder theorem for pairwise distinct primes (IsDedekindDomain.exists_forall_sub_mem_ideal).

Main results

• IsDedekindDomain.HeightOneSpectrum.exists_forall_valued_sub_le: finitely many local integers are simultaneously approximated by one element of R.
• IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap_pi: the diagonal image of R is dense in the product of the completed integer rings at a finite set of places.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §3 (the Chinese remainder theorem).

theorem IsDedekindDomain.HeightOneSpectrum.exists_forall_valued_sub_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (s : Finset (HeightOneSpectrum R)) (x : (v : HeightOneSpectrum R) → ↥(adicCompletionIntegers K v)) (n : HeightOneSpectrum R → ℕ) : ∃ (r : R), ∀ v ∈ s, Valued.v (↑(x v) - (algebraMap R (adicCompletion K v)) r) ≤ WithZero.exp (-↑(n v))

Simultaneous approximation by elements of R. Finitely many elements of the rings of integers 𝒪_v of the completions of K are approximated by a single element of R, to any prescribed precision at each of the finitely many places.

theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap_pi_subtype {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (p : HeightOneSpectrum R → Prop) : DenseRange fun (x : R) (v : { v : HeightOneSpectrum R // p v }) => (algebraMap R ↥(adicCompletionIntegers K ↑v)) x

The diagonal image of a Dedekind domain is dense in the product of the completed integer rings over any subtype of its height one primes. Product neighborhoods involve only finitely many coordinates, so no finiteness assumption on the subtype is needed.

theorem IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap_pi {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (s : Finset (HeightOneSpectrum R)) : DenseRange fun (x : R) (v : ↥s) => (algebraMap R ↥(adicCompletionIntegers K ↑v)) x

The diagonal image of a Dedekind domain is dense in the product of the completed integer rings at any finite set of height one primes.