Siegel's lemma, in height form

Mathlib proves the classical Siegel lemma as a statement about the sup norm: a nonzero M × N integer matrix with M < N kills a nonzero integer vector of norm at most (N ‖A‖) ^ (M / (N - M)). This file restates it in the vocabulary of heights, which is what the rest of the roadmap consumes; the translation between the two normalizations is isolated as a lemma of its own, the exponent is shown to be sharp, and the number-field corollary is read off Mathlib's house-normalized version the same way.

Main results

• Rat.gcd_mul_mulHeight_intCast: the translation. For a nonzero integer tuple, gcd x * H(x) = max i, |x i|; Rat.mulHeight_intCast_le is the inequality it is used through.
• Int.Matrix.exists_ne_zero_mulVec_eq_zero_iSup_abs_le and Int.Matrix.exists_ne_zero_mulVec_eq_zero_mulHeight_le: Siegel's lemma with an explicit bound B on the entries, in the sup norm and in the height, both at (N B) ^ (M / (N - M)).
• Int.Matrix.exists_forall_pow_le_iSup_abs: the exponent M / (N - M) is sharp.
• NumberField.absMulHeight_le_iSup_house: the absolute height of a tuple of algebraic integers is at most the largest house of its entries.
• NumberField.exists_forall_exists_ne_zero_mulVec_eq_zero_absMulHeight_le: Siegel's lemma over a number field in height form, Bombieri–Gubler's Corollary 2.9.2.

Implementation notes

⚠ The height form is not a strengthening, because the content can always be divided out. The height of an integer tuple is its sup norm divided by the greatest common divisor of its entries, so H(x) ≤ max i, |x i| with equality exactly on primitive tuples. That makes the height bound formally weaker-looking hypotheses and formally stronger conclusions, but nothing is gained: the primitive multiple of a kernel vector is again a kernel vector, and it is the one on which the two statements coincide. What the translation buys is the vocabulary: everything downstream of Layer 1 is stated for Height.mulHeight, and a sup norm cannot be fed to it.

⚠ The exponent is sharp already at N = M + 1, and only the factor N ^ (M / (N - M)) is slack. The equations B xᵢ = xᵢ₊₁ have kernel the line through (1, B, B², …, B ^ M), whose nonzero integer points all have sup norm at least B ^ M, against the bound ((M + 1) B) ^ M. Taking k such blocks side by side realizes every exponent M = k M / (k (M + 1) - k M), so the sharpness is not an artifact of N - M = 1. The bound is nevertheless not invariant: it changes under A ↦ U A for U ∈ GL_M(ℤ), which leaves the kernel alone, and removing that defect is the whole content of Layer 5.2.

⚠ Passing from the house to the height costs no constant at all. For a tuple of algebraic integers every finite local factor is at most 1 — the finite part of the height is the inverse norm of the ideal the entries generate, and that norm is a positive integer — while each infinite place is the modulus of a conjugate and so is dominated by the house. The infinite factors carry the weights mult v, which sum to [K : ℚ], and that is exactly the root the absolute normalization takes. So H_abs(x) ≤ max l, house (x l) with no degree factor, and Mathlib's number-field Siegel bound transfers verbatim.

⚠ Mathlib's number-field constant is private. c₁ K of Mathlib/NumberTheory/NumberField/House.lean cannot be named from outside that file, so the restatement has to quantify over it existentially — which is also the shape Bombieri–Gubler state the corollary in — and the witness is supplied by unification against the theorem it is proved from.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Lemma 2.9.1 and Corollary 2.9.2.

M. Hindry and J. H. Silverman, Diophantine Geometry: An Introduction, Springer (2000), Lemma D.4.1, which is the statement Mathlib's file is proved against.

This is Layer 5.1 of the ArithmeticHeights roadmap.

The sup norm of an integer tuple

theorem Int.pi_norm_eq_iSup_abs {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ι → ℤ) : ‖x‖ = ↑(⨆ (i : ι), |x i|)

The sup norm of an integer tuple is the maximum of the absolute values of its entries. The left-hand side is the shape Mathlib's Siegel lemma is stated in, the right-hand side the shape every height statement is stated in.

theorem Rat.gcd_mul_mulHeight_intCast {ι : Type u_1} [Nonempty ι] {x : ι → ℤ} [Fintype ι] (hx : x ≠ 0) : ↑(Finset.univ.gcd x) * Height.mulHeight (Int.cast ∘ x) = ↑(⨆ (i : ι), |x i|)

The sup-norm-to-height translation. The multiplicative height of a nonzero tuple of integers, read as a tuple of rationals, is the maximum of the absolute values of its entries divided by their greatest common divisor. Mathlib's Rat.mulHeight_eq_max_abs_of_gcd_eq_one is the primitive case; the content is what the projective height divides out.

theorem Rat.mulHeight_intCast_le {ι : Type u_1} [Nonempty ι] {x : ι → ℤ} [Finite ι] (hx : x ≠ 0) : Height.mulHeight (Int.cast ∘ x) ≤ ↑(⨆ (i : ι), |x i|)

The height of an integer tuple is at most its sup norm, with equality exactly when the tuple is primitive. This is the direction Siegel's lemma is read in.

Siegel's lemma in height form

theorem Int.Matrix.exists_ne_zero_mulVec_eq_zero_iSup_abs_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (A : Matrix α β ℤ) {B : ℤ} (hB : 1 ≤ B) (hA : ∀ (i : α) (j : β), |A i j| ≤ B) (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) : ∃ (x : β → ℤ), x ≠ 0 ∧ A.mulVec x = 0 ∧ ↑(⨆ (j : β), |x j|) ≤ (↑(Fintype.card β) * ↑B) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))

Siegel's lemma, with an explicit bound on the entries. A system of M linear equations in N > M unknowns with integer coefficients of absolute value at most B has a nonzero integer solution of sup norm at most (N B) ^ (M / (N - M)).

This is Mathlib's Int.Matrix.exists_ne_zero_int_vec_norm_le with the matrix norm traded for a bound on the entries; the hypothesis 1 ≤ B is what removes the max 1 ‖A‖ there, and costs nothing, since a nonzero integer matrix has an entry of absolute value at least 1.

theorem Int.Matrix.exists_ne_zero_mulVec_eq_zero_mulHeight_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (A : Matrix α β ℤ) {B : ℤ} (hB : 1 ≤ B) (hA : ∀ (i : α) (j : β), |A i j| ≤ B) (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) : ∃ (x : β → ℤ), x ≠ 0 ∧ A.mulVec x = 0 ∧ Height.mulHeight (Int.cast ∘ x) ≤ (↑(Fintype.card β) * ↑B) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))

Siegel's lemma in height form (Bombieri–Gubler, Lemma 2.9.1; Hindry–Silverman, Lemma D.4.1). The solution the previous statement produces has multiplicative height at most (N B) ^ (M / (N - M)) as well: by Rat.gcd_mul_mulHeight_intCast the height of an integer tuple is at most its sup norm, and the two agree when the tuple is primitive — which the minimal solution is, but which the statement does not need.

theorem Int.Matrix.exists_forall_pow_le_iSup_abs (M : ℕ) {B : ℤ} (hB : 1 ≤ B) : ∃ (A : Matrix (Fin M) (Fin (M + 1)) ℤ), (∀ (i : Fin M) (j : Fin (M + 1)), |A i j| ≤ B) ∧ ∀ (x : Fin (M + 1) → ℤ), x ≠ 0 → A.mulVec x = 0 → B ^ M ≤ ⨆ (j : Fin (M + 1)), |x j|

The exponent M / (N - M) is sharp, already for N = M + 1, where it is M. The M × (M + 1) matrix of the equations B xᵢ = xᵢ₊₁ has entries of absolute value at most B and kernel the line spanned by (1, B, B², …, B ^ M), so every nonzero solution has sup norm at least B ^ M, against a bound of ((M + 1) B) ^ M: only the factor (M + 1) ^ M is slack.

Taking k copies of this system side by side gives, for every k, an k M × k (M + 1) system with the same conclusion and exponent k M / k = M, so no exponent below M / (N - M) can be substituted in the statement above.

Siegel's lemma over a number field

theorem NumberField.absMulHeight_le_iSup_house {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x : ι → RingOfIntegers K} (hx : x ≠ 0) : (absMulHeight fun (i : ι) => ↑(x i)) ≤ ⨆ (i : ι), house ↑(x i)

The house bounds the height. For a nonzero tuple of algebraic integers the absolute multiplicative height is at most the largest house of its entries: the finite local factors are at most 1 because the entries are integral, and each infinite one is bounded by the house because an infinite place is the modulus of a conjugate.

This is the whole of the passage from Mathlib's NumberField.house-normalized Siegel lemma to a height statement.

theorem NumberField.exists_forall_exists_ne_zero_mulVec_eq_zero_absMulHeight_le (K : Type u_3) [Field K] [NumberField K] : ∃ (C : ℝ), ∀ (p q : ℕ) (a : Matrix (Fin p) (Fin q) (RingOfIntegers K)) (A : ℝ), a ≠ 0 → 0 < p → p < q → (∀ (k : Fin p) (l : Fin q), house ↑(a k l) ≤ A) → ∃ (ξ : Fin q → RingOfIntegers K), ξ ≠ 0 ∧ a.mulVec ξ = 0 ∧ (absMulHeight fun (l : Fin q) => ↑(ξ l)) ≤ C * (C * ↑q * A) ^ (↑p / (↑q - ↑p))

Siegel's lemma over a number field, in height form (Bombieri–Gubler, Corollary 2.9.2). There is a constant C, depending only on K, such that a system of p linear equations in q > p unknowns whose coefficients are algebraic integers of house at most A has a nonzero solution in 𝓞 K ^ q of absolute multiplicative height at most C (C q A) ^ (p / (q - p)).

The constant is Mathlib's, and is private in Mathlib/NumberTheory/NumberField/House.lean; quantifying over it existentially is therefore the only way to restate the theorem, and it is also the shape the literature states it in. What is proved here is the left-hand side: Mathlib bounds the house of each coordinate, and absMulHeight_le_iSup_house turns that into a bound on the height of the tuple.