Evertse's lemma over a number field

Let K be a number field, S₀ a finite set of finite places, and x 0, …, x (m - 1) a basis of a K-vector space V. At every infinite place and every place of S₀ let m linearly independent linear forms L v k on V, weights ν v k > 0 and a nondecreasing sequence μ v satisfy |L v k (x j)|_v ≤ ν v k * μ v j. Evertse's lemma (NumberField.exists_evertse) corrects the basis to

y j = x j + ∑ l < j, ξ j l • x l, with every ξ j l integral outside S₀,

and reorders the forms at each place by a permutation π v, so that

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

at the infinite places and the same bound without C at the places of S₀. The constant C depends only on K and m: it is chosen before S₀, the space, the forms and the basis. NumberField.exists_evertse_unweighted is the case ν = 1.

In the proof of Schmidt's Subspace Theorem the lemma is applied to a family realizing the successive minima of a parallelepiped, with weights ν v i = Q ^ c v i that change with the level Q; this is why the constant must be uniform. It replaces Mahler's theorem on compound bodies and Davenport's lemma in Schmidt's original argument. The proof is the general AbsoluteValue.exists_evertse_of_approx, fed with simultaneous approximation by S₀-integers, NumberField.exists_forall_apply_add_le.

Main results

• NumberField.exists_evertse: Evertse's lemma with weights.
• NumberField.exists_evertse_unweighted: Evertse's lemma without weights.

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_evertse {K : Type u_1} [Field K] [NumberField K] (m : ℕ) : ∃ (C : ℝ), ∀ (V : Type u_2) [inst : AddCommGroup V] [inst_1 : Module K V] (Sfin : Finset (FinitePlace K)) (L : AbsoluteValue K ℝ → Fin m → Module.Dual K V) (x : Module.Basis (Fin m) K V) (ν μ : AbsoluteValue K ℝ → Fin m → ℝ), (∀ (v : InfinitePlace K), LinearIndependent K (L ↑v)) → (∀ v ∈ Sfin, LinearIndependent K (L ↑v)) → (∀ (v : InfinitePlace K) (k : Fin m), 0 < ν (↑v) k) → (∀ v ∈ Sfin, ∀ (k : Fin m), 0 < ν (↑v) k) → (∀ (v : InfinitePlace K), Monotone (μ ↑v)) → (∀ v ∈ Sfin, Monotone (μ ↑v)) → (∀ (v : InfinitePlace K) (k j : Fin m), v ((L (↑v) k) (x j)) ≤ ν (↑v) k * μ (↑v) j) → (∀ v ∈ Sfin, ∀ (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), ∀ u ∉ Sfin, u (ξ j l) ≤ 1) ∧ (∀ (v : InfinitePlace K) (i j : Fin m), v ((L (↑v) ((π ↑v) i)) (x j + ∑ l : Fin m with l < j, ξ j l • x l)) ≤ C * (ν (↑v) ((π ↑v) i) * min (μ (↑v) i) (μ (↑v) j))) ∧ ∀ v ∈ Sfin, ∀ (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). There is a constant C, depending only on K and m, with the following property. Let S₀ be a finite set of finite places, x a basis of a K-vector space V indexed by Fin m, and at every infinite place and every place of S₀ let the forms L v k be linearly independent, the weights ν v k positive and μ v nondecreasing, with |L v k (x j)|_v ≤ ν v k * μ v j. Then there are ξ j l ∈ K, integral outside S₀, and permutations π v, such that y j = x j + ∑ l < j, ξ j l • x l satisfies |L v (π v i) (y j)|_v ≤ C * (ν v (π v i) * min (μ v i) (μ v j)) at every infinite place and |L v (π v i) (y j)|_v ≤ ν v (π v i) * min (μ v i) (μ v j) at every place of S₀.

theorem NumberField.exists_evertse_unweighted {K : Type u_1} [Field K] [NumberField K] (m : ℕ) : ∃ (C : ℝ), ∀ (V : Type u_2) [inst : AddCommGroup V] [inst_1 : Module K V] (Sfin : Finset (FinitePlace K)) (L : AbsoluteValue K ℝ → Fin m → Module.Dual K V) (x : Module.Basis (Fin m) K V) (μ : AbsoluteValue K ℝ → Fin m → ℝ), (∀ (v : InfinitePlace K), LinearIndependent K (L ↑v)) → (∀ v ∈ Sfin, LinearIndependent K (L ↑v)) → (∀ (v : InfinitePlace K), Monotone (μ ↑v)) → (∀ v ∈ Sfin, Monotone (μ ↑v)) → (∀ (v : InfinitePlace K) (k j : Fin m), v ((L (↑v) k) (x j)) ≤ μ (↑v) j) → (∀ v ∈ Sfin, ∀ (k j : Fin m), v ((L (↑v) k) (x j)) ≤ μ (↑v) j) → ∃ (ξ : Fin m → Fin m → K) (π : AbsoluteValue K ℝ → Equiv.Perm (Fin m)), (∀ (j l : Fin m), ∀ u ∉ Sfin, u (ξ j l) ≤ 1) ∧ (∀ (v : InfinitePlace K) (i j : Fin m), v ((L (↑v) ((π ↑v) i)) (x j + ∑ l : Fin m with l < j, ξ j l • x l)) ≤ C * min (μ (↑v) i) (μ (↑v) j)) ∧ ∀ v ∈ Sfin, ∀ (i j : Fin m), v ((L (↑v) ((π ↑v) i)) (x j + ∑ l : Fin m with l < j, ξ j l • x l)) ≤ min (μ (↑v) i) (μ (↑v) j)

Evertse's lemma without weights (Evertse; Bombieri–Gubler, Lemma 7.5.29): the case ν = 1 of NumberField.exists_evertse. If |L v k (x j)|_v ≤ μ v j with μ v nondecreasing, then the corrected basis satisfies |L v (π v i) (y j)|_v ≤ C * min (μ v i) (μ v j) at the infinite places and |L v (π v i) (y j)|_v ≤ min (μ v i) (μ v j) at the places of S₀.