Evertse's lemma for a field with simultaneous approximation

Let K be a field, V a K-vector space with linearly independent vectors x 0, …, x (m - 1), and let T be a set of absolute values on K. At each v ∈ T let m linear forms L v k separate the points of V, let weights ν v k > 0 and a nondecreasing sequence μ v 0 ≤ … ≤ μ v (m - 1) bound the values v (L v k (x j)) ≤ ν v k * μ v j. Evertse's lemma replaces x by vectors

y j = x j + ∑ l < j, ξ j l • x l

with coefficients ξ j l in a subset R ⊆ K and reorders the forms at each place by a permutation π v, so that every value is bounded by the smaller of the two relevant sequence terms:

v (L v (π v i) (y j)) ≤ C * ν v (π v i) * min (μ v i) (μ v j).

The only arithmetic input is that R approximates every family of targets at the places of T simultaneously: for every γ some ξ ∈ R has v (ξ + γ v) ≤ A v for all v ∈ T (AbsoluteValue.exists_evertse_of_approx). The constant is C = 2 ^ (2 m + 1) * max 1 (A v) at every place, and C = 1 at a nonarchimedean place where A v ≤ 1.

Over a number field, with R the elements integral outside a finite set of finite places, this is the form of Evertse's lemma that replaces Mahler's theorem on compound bodies and Davenport's lemma in the proof of Schmidt's Subspace Theorem: it turns a family of vectors realizing the successive minima of a parallelepiped into one whose exterior products are controlled.

The proof has two steps.

• At one place the vectors are made exactly triangular: column elimination with partial pivoting, where the pivot row for x j maximizes v (L v r (·)) / ν v r, produces z j ∈ x j + span (x l, l < j) with L v (π i) (z j) = 0 for i < j, at the cost of a factor 2 per elimination step, or 1 when v is nonarchimedean.
• These local triangular families are glued by approximation: the coefficients ξ j l are chosen from l = j - 1 down to 0, each one approximating at every place at once the coordinate of the remaining error on z l, so that y j - z j is a combination of the z l, l < j, with coefficients of size at most A v at v.

Main results

• AbsoluteValue.exists_evertse_of_approx: Evertse's lemma for any field and any set of absolute values admitting simultaneous approximation by a subset R.

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 AbsoluteValue.exists_evertse_of_approx {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {m : ℕ} {T : Set (AbsoluteValue K ℝ)} {R : Set K} {A : AbsoluteValue K ℝ → ℝ} (happrox : ∀ (γ : AbsoluteValue K ℝ → K), ∃ ξ ∈ R, ∀ v ∈ T, v (ξ + γ v) ≤ A v) {L : AbsoluteValue K ℝ → Fin m → Module.Dual K V} (hL : ∀ v ∈ T, ∀ (z : V), (∀ (k : Fin m), (L v k) z = 0) → z = 0) {x : Fin m → V} (hx : LinearIndependent K x) {ν μ : AbsoluteValue K ℝ → Fin m → ℝ} (hν : ∀ v ∈ T, ∀ (k : Fin m), 0 < ν v k) (hμ : ∀ v ∈ T, Monotone (μ v)) (hLx : ∀ v ∈ T, ∀ (k j : Fin m), v ((L v k) (x j)) ≤ ν v k * μ v j) : ∃ (ξ : Fin m → Fin m → K) (π : AbsoluteValue K ℝ → Equiv.Perm (Fin m)), (∀ (j l : Fin m), ξ j l ∈ R) ∧ (∀ v ∈ T, ∀ (i j : Fin m), v ((L v ((π v) i)) (x j + ∑ l : Fin m with l < j, ξ j l • x l)) ≤ 2 ^ (2 * m + 1) * max 1 (A v) * (ν v ((π v) i) * min (μ v i) (μ v j))) ∧ ∀ v ∈ T, IsNonarchimedean ⇑v → A v ≤ 1 → ∀ (i j : Fin m), v ((L v ((π v) i)) (x j + ∑ l : Fin m with l < j, ξ j l • x l)) ≤ ν v ((π v) i) * min (μ v i) (μ v j)

Evertse's lemma (Evertse; Bombieri–Gubler, Lemma 7.5.29), for a field K with a set T of absolute values at which a subset R approximates every family of targets simultaneously, v (ξ + γ v) ≤ A v. Let x 0, …, x (m - 1) be linearly independent in V, and at each v ∈ T let the forms L v k separate the points of V, with weights ν v k > 0 and a nondecreasing μ v bounding v (L v k (x j)) ≤ ν v k * μ v j. Then there are coefficients ξ j l ∈ R and permutations π v such that y j = x j + ∑ l < j, ξ j l • x l satisfies v (L v (π v i) (y j)) ≤ 2 ^ (2 m + 1) * max 1 (A v) * (ν v (π v i) * min (μ v i) (μ v j)) at every v ∈ T, and the same bound without the constant at every nonarchimedean v ∈ T with A v ≤ 1.