Siegel's lemma over a number field with rational integer unknowns

Let K be a number field of degree d and let a be an M × N matrix over 𝓞 K whose entries have house at most A ≥ 1. If d * M < N, the system a x = 0 has a nonzero solution x ∈ ℤ^N with |xⱼ| ≤ (3 N A) ^ (d M / (N - d M)) for every j. The unknowns are rational integers, and the constant depends only on N and A, not on a choice of integral basis of K. This is the form of Siegel's lemma used to construct auxiliary polynomials with integer coefficients, for instance in the proof of Roth's theorem.

Mathlib's NumberField.house.exists_ne_zero_int_vec_house_le solves the same system with unknowns in 𝓞 K and a constant depending on an integral basis; Mathlib's Int.Matrix.exists_ne_zero_int_vec_norm_le is the case of integer coefficients.

The proof is a pigeonhole argument in the coordinates of Mathlib's mixedEmbedding.stdBasis: an algebraic integer has d such real coordinates, and it vanishes as soon as all of them are at most 2 / 3 in absolute value, because then every conjugate has modulus at most 2 √2 / 3 < 1.

Main results

• NumberField.mixedEmbedding.abs_stdBasis_repr_le_house: every stdBasis coordinate of the mixed embedding of x is bounded by the house of x.
• NumberField.mixedEmbedding.stdBasis_repr_mulVec_intCast: the stdBasis coordinates of the mixed embedding of a *ᵥ x, for an integer vector x, are ℤ-linear combinations of those of the entries of a.
• NumberField.RingOfIntegers.eq_zero_of_abs_stdBasis_repr_le: an algebraic integer whose stdBasis coordinates are all at most 2 / 3 in absolute value is zero.
• NumberField.RingOfIntegers.eq_zero_of_abs_re_le_of_abs_im_le: an algebraic integer whose conjugates all have real and imaginary parts at most 2 / 3 in absolute value is zero.
• NumberField.exists_ne_zero_int_vec_abs_le_of_house_le: Siegel's lemma over K with unknowns in ℤ.
• NumberField.sum_mul_intCast_eq_zero_of_mulVec_eq_zero: such a solution satisfies each row equation ∑ⱼ aᵢⱼ xⱼ = 0 in K.

References

• J.-H. Evertse, Diophantine approximation and transcendence theory, lecture notes (2019), Chapter 3, Lemma 3.19 and Theorem 3.20.
• The counting estimate follows the proof of Int.Matrix.exists_ne_zero_int_vec_norm_le in Mathlib (F. Barroero, L. Capuano, A. Turchet).

theorem NumberField.mixedEmbedding.abs_stdBasis_repr_le_house {K : Type u_1} [Field K] [NumberField K] (x : K) (r : index K) : |((stdBasis K).repr ((mixedEmbedding K) x)) r| ≤ house x

Every coordinate of the mixed embedding of x in stdBasis is bounded in absolute value by the house of x.

theorem NumberField.mixedEmbedding.stdBasis_repr_mulVec_intCast {K : Type u_1} [Field K] [NumberField K] {α : Type u_2} {β : Type u_3} [Fintype β] (a : Matrix α β (RingOfIntegers K)) (x : β → ℤ) (i : α) (r : index K) : ((stdBasis K).repr ((mixedEmbedding K) ↑(a.mulVec (fun (j : β) => ↑(x j)) i))) r = ∑ j : β, ↑(x j) * ((stdBasis K).repr ((mixedEmbedding K) ↑(a i j))) r

The stdBasis coordinates of the mixed embedding of a *ᵥ x are the corresponding ℤ-linear combinations of the coordinates of the entries of a.

theorem NumberField.RingOfIntegers.eq_zero_of_abs_stdBasis_repr_le {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} (h : ∀ (r : mixedEmbedding.index K), |((mixedEmbedding.stdBasis K).repr ((mixedEmbedding K) ↑x)) r| ≤ 2 / 3) : x = 0

An algebraic integer whose real coordinates (stdBasis K).repr (mixedEmbedding K x) are all at most 2 / 3 in absolute value is zero: each of its conjugates then has modulus at most 2 √2 / 3 < 1.

theorem NumberField.RingOfIntegers.eq_zero_of_abs_re_le_of_abs_im_le {K : Type u_1} [Field K] [NumberField K] {x : RingOfIntegers K} (hre : ∀ (σ : K →+* ℂ), |(σ ↑x).re| ≤ 2 / 3) (him : ∀ (σ : K →+* ℂ), |(σ ↑x).im| ≤ 2 / 3) : x = 0

Evertse, Lemma 3.19. An algebraic integer x such that every complex embedding σ satisfies |Re σ(x)| ≤ 2 / 3 and |Im σ(x)| ≤ 2 / 3 is zero.

theorem NumberField.exists_ne_zero_int_vec_abs_le_of_house_le {K : Type u_1} [Field K] [NumberField K] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (a : Matrix α β (RingOfIntegers K)) {A : ℝ} (hA : 1 ≤ A) (hcard : Module.finrank ℚ K * Fintype.card α < Fintype.card β) (ha : ∀ (i : α) (j : β), house ↑(a i j) ≤ A) : ∃ (x : β → ℤ), x ≠ 0 ∧ (a.mulVec fun (j : β) => ↑(x j)) = 0 ∧ ∀ (j : β), |↑(x j)| ≤ (3 * ↑(Fintype.card β) * A) ^ (↑(Module.finrank ℚ K) * ↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Module.finrank ℚ K) * ↑(Fintype.card α)))

Siegel's lemma over a number field, with rational integer unknowns (Evertse, Theorem 3.20). Let K be a number field of degree d and a a matrix over 𝓞 K with M rows and N columns, whose entries have house at most A ≥ 1. If d * M < N, there is a nonzero x ∈ ℤ^N with a x = 0 and |xⱼ| ≤ (3 N A) ^ (d M / (N - d M)) for every j.

theorem NumberField.sum_mul_intCast_eq_zero_of_mulVec_eq_zero {K : Type u_1} [Field K] {α : Type u_2} {β : Type u_3} [Fintype β] {a : Matrix α β (RingOfIntegers K)} {x : β → ℤ} (hax : (a.mulVec fun (j : β) => ↑(x j)) = 0) (i : α) : ∑ j : β, ↑(a i j) * ↑(x j) = 0

An integer solution x of a x = 0 over 𝓞 K solves every row equation in K: ∑ⱼ aᵢⱼ xⱼ = 0.