Simultaneous approximation by S-integers

Let K be a number field and S a finite set of finite places of K. Given an element γ v of K for each place v in S and for each infinite place, some ξ ∈ K is integral at every finite place outside S, satisfies |ξ + γ v|_v ≤ 1 at every v ∈ S, and satisfies |ξ + γ v|_v ≤ A at every infinite place, where A depends on K alone and not on S or on the γ v (NumberField.exists_forall_apply_add_le). Thus -γ is approximated by a single S-integer at the places of S and at the infinite places at once, with a uniform loss at the infinite places.

This is the approximation step in the proof of Evertse's lemma (Bombieri–Gubler, Lemma 7.5.29), where a basis is corrected by S-integral multiples of earlier vectors; the constant is uniform in S and in the targets because the lemma is applied to forms which change with a parameter.

The proof has two halves.

• At the finite places, NumberField.exists_forall_finitePlace_apply_add_le_one is strong approximation for the finite adeles, IsDedekindDomain.FiniteAdeleRing.exists_forall_sub_algebraMap_mem_adicCompletionIntegers, applied to the finite adele with component -γ v at the places of S and 0 elsewhere.
• At the infinite places, NumberField.exists_integer_forall_infinitePlace_add_le translates by an algebraic integer ω, which changes no finite condition, so that the vector of the ω + γ v lands in the fundamental domain of the Minkowski lattice of 𝓞 K. The constant is the sum of the norms of the embedded integral basis mixedEmbedding.latticeBasis K.

Main results

• NumberField.exists_forall_finitePlace_apply_add_le_one: an element of K integral outside S and within 1 of -γ v at every place of S.
• NumberField.exists_integer_forall_infinitePlace_add_le: an algebraic integer within ∑ i, ‖mixedEmbedding.latticeBasis K i‖ of -γ v at every infinite place.
• NumberField.exists_forall_apply_add_le: the two combined, with a constant chosen before S and the targets.

References

• J.-H. Evertse, An improvement of the quantitative Subspace theorem, Compositio Math. 101 (1996), 225–311.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006, Lemma 7.5.29.

theorem NumberField.exists_forall_finitePlace_apply_add_le_one {K : Type u_1} [Field K] [NumberField K] (S : Finset (FinitePlace K)) (γ : FinitePlace K → K) : ∃ (ξ : K), (∀ v ∉ S, v ξ ≤ 1) ∧ ∀ v ∈ S, v (ξ + γ v) ≤ 1

Approximation at finitely many finite places by an element integral elsewhere. For a finite set S of finite places and targets γ v ∈ K, some ξ ∈ K is integral at every finite place outside S and satisfies |ξ + γ v|_v ≤ 1 at every place v of S.

theorem NumberField.exists_integer_forall_infinitePlace_add_le {K : Type u_1} [Field K] [NumberField K] (γ : InfinitePlace K → K) : ∃ (ω : RingOfIntegers K), ∀ (v : InfinitePlace K), v (↑ω + γ v) ≤ ∑ i : Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K), ‖(mixedEmbedding.latticeBasis K) i‖

Approximation at the infinite places by an algebraic integer. For targets γ v ∈ K at the infinite places, some ω ∈ 𝓞 K satisfies |ω + γ v|_v ≤ A at every infinite place v, where A = ∑ i, ‖mixedEmbedding.latticeBasis K i‖ is the sum of the norms of the embedded integral basis.

theorem NumberField.exists_forall_apply_add_le {K : Type u_1} [Field K] [NumberField K] : ∃ (A : ℝ), ∀ (S : Finset (FinitePlace K)) (γ : AbsoluteValue K ℝ → K), ∃ (ξ : K), (∀ v ∉ S, v ξ ≤ 1) ∧ (∀ v ∈ S, v (ξ + γ ↑v) ≤ 1) ∧ ∀ (v : InfinitePlace K), v (ξ + γ ↑v) ≤ A

Simultaneous approximation by S-integers (the approximation step of Evertse's lemma, Bombieri–Gubler, Lemma 7.5.29). There is a constant A, depending only on K, such that for every finite set S of finite places and all targets γ, some ξ ∈ K is integral at every finite place outside S, satisfies |ξ + γ v|_v ≤ 1 at every v ∈ S and |ξ + γ v|_v ≤ A at every infinite place. The targets are indexed by the underlying absolute values of the places, so that one family serves both kinds of place; its values elsewhere are irrelevant.