Polynomials of bounded partial degrees and the vanishing conditions of the index

The auxiliary polynomial of Roth's method is bounded one variable at a time, degreeOf j P ≤ d j, rather than in total degree. Its coefficients therefore sit on the box ∏ j, {0, …, d j} of exponents, and this file is the dictionary between coefficient vectors on that box and polynomials. The box is named by the Pi type ∀ j, Fin (d j + 1), so that its cardinality is ∏ j, (d j + 1) by Fintype.card_pi, and a vector indexed by it is a function of one index per variable.

Through this dictionary, the vanishing of a Hasse derivative ∂^μ P at a point α becomes a linear condition on the coefficient vector of P: its row has the entry ∏ j, (I j choose μ j) α j ^ (I j - μ j) at the exponent I. A polynomial of prescribed index at several points is then a nonzero vector in the kernel of finitely many such rows, which is what Siegel's lemma produces. The rows are products over the variables of rows in one variable, and that is what makes their heights computable (MvPolynomial.mulHeight_hasseDerivRow_le in TauCeti/NumberTheory/Height/MvPolynomial.lean).

Main definitions

• MvPolynomial.boxMonomial d I: the exponent named by a point I of the box.
• MvPolynomial.ofBox d: the linear map sending a coefficient vector on the box to its polynomial.
• MvPolynomial.hasseDerivRow d α μ: the row of the condition "∂^μ P vanishes at α".

Main results

• MvPolynomial.coeff_ofBox, MvPolynomial.coeff_ofBox_of_not_le, MvPolynomial.degreeOf_ofBox_le, MvPolynomial.ofBox_coeff, MvPolynomial.ofBox_injective and MvPolynomial.range_ofBox: ofBox d is injective with image the polynomials whose partial degrees are bounded by d, that is restrictSupport R {ν | ∀ j, ν j ≤ d j}.
• MvPolynomial.aeval_hasseDeriv_ofBox and MvPolynomial.aeval_hasseDeriv_eq_sum: the value at α of a Hasse derivative of a polynomial of the box is the row hasseDerivRow d α μ applied to its coefficient vector. The point may lie in any algebra over the coefficients, which is how a polynomial over a number field K is tested at points of an extension of K.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Lemma 6.3.4.
• The statements follow DiophantineApproximation/BoxMonomial.lean and DiophantineApproximation/IndexConditions.lean of Ralf Stephan's rwst/Subspace-Theorems, commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338 (Apache 2.0).

The exponents of the box

noncomputable def MvPolynomial.boxMonomial {σ : Type u_1} [Finite σ] (d : σ → ℕ) (I : (j : σ) → Fin (d j + 1)) : σ →₀ ℕ

The exponent named by a point I of the box ∀ j, Fin (d j + 1): the exponent of X j is I j.

@[simp]

theorem MvPolynomial.boxMonomial_apply {σ : Type u_1} [Finite σ] (d : σ → ℕ) (I : (j : σ) → Fin (d j + 1)) (j : σ) : (boxMonomial d I) j = ↑(I j)

theorem MvPolynomial.boxMonomial_le {σ : Type u_1} [Finite σ] (d : σ → ℕ) (I : (j : σ) → Fin (d j + 1)) (j : σ) : (boxMonomial d I) j ≤ d j

Every exponent named by the box lies in the box.

theorem MvPolynomial.boxMonomial_injective {σ : Type u_1} [Finite σ] {d : σ → ℕ} : Function.Injective (boxMonomial d)

Distinct points of the box name distinct exponents.

theorem MvPolynomial.range_boxMonomial {σ : Type u_1} [Finite σ] {d : σ → ℕ} : Set.range (boxMonomial d) = {ν : σ →₀ ℕ | ∀ (j : σ), ν j ≤ d j}

The exponents named by the box are exactly the exponents bounded by d.

theorem MvPolynomial.exists_boxMonomial_eq {σ : Type u_1} [Finite σ] {d : σ → ℕ} {ν : σ →₀ ℕ} (h : ∀ (j : σ), ν j ≤ d j) : ∃ (I : (j : σ) → Fin (d j + 1)), boxMonomial d I = ν

Every exponent bounded by d is named by the box.

theorem MvPolynomial.exists_boxMonomial_eq_of_mem_support {σ : Type u_1} [Finite σ] {d : σ → ℕ} {R : Type u_2} [CommSemiring R] {P : MvPolynomial σ R} (hP : ∀ (j : σ), degreeOf j P ≤ d j) {ν : σ →₀ ℕ} (hν : ν ∈ P.support) : ∃ (I : (j : σ) → Fin (d j + 1)), boxMonomial d I = ν

The exponents of a polynomial whose partial degrees are bounded by d are named by the box.

Coefficient vectors on the box

noncomputable def MvPolynomial.ofBox {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] (d : σ → ℕ) : (((j : σ) → Fin (d j + 1)) → R) →ₗ[R] MvPolynomial σ R

The polynomial ∑ I, x I • X ^ (boxMonomial d I) with coefficient vector x on the box ∀ j, Fin (d j + 1).

theorem MvPolynomial.ofBox_apply {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} (x : ((j : σ) → Fin (d j + 1)) → R) : (ofBox d) x = ∑ I : (j : σ) → Fin (d j + 1), (monomial (boxMonomial d I)) (x I)

@[simp]

theorem MvPolynomial.map_ofBox {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} {S : Type u_3} [CommSemiring S] (f : R →+* S) (x : ((j : σ) → Fin (d j + 1)) → R) : (map f) ((ofBox d) x) = (ofBox d) fun (I : (j : σ) → Fin (d j + 1)) => f (x I)

Mapping the coefficients of a polynomial on a box maps its coefficient vector entrywise.

@[simp]

theorem MvPolynomial.coeff_ofBox {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} (x : ((j : σ) → Fin (d j + 1)) → R) (I : (j : σ) → Fin (d j + 1)) : ((ofBox d) x).coeff (boxMonomial d I) = x I

theorem MvPolynomial.coeff_ofBox_of_not_le {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} (x : ((j : σ) → Fin (d j + 1)) → R) {ν : σ →₀ ℕ} (hν : ¬∀ (j : σ), ν j ≤ d j) : ((ofBox d) x).coeff ν = 0

Outside the box, the polynomial with a given coefficient vector has no coefficients.

theorem MvPolynomial.ofBox_mem_restrictSupport {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} (x : ((j : σ) → Fin (d j + 1)) → R) : (ofBox d) x ∈ restrictSupport R {ν : σ →₀ ℕ | ∀ (j : σ), ν j ≤ d j}

The polynomial with a coefficient vector on the box has its support in the box.

theorem MvPolynomial.degreeOf_ofBox_le {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} (x : ((j : σ) → Fin (d j + 1)) → R) (j : σ) : degreeOf j ((ofBox d) x) ≤ d j

The polynomial with a coefficient vector on the box has partial degrees bounded by d.

theorem MvPolynomial.ofBox_coeff {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} {P : MvPolynomial σ R} (hP : ∀ (j : σ), degreeOf j P ≤ d j) : ((ofBox d) fun (I : (j : σ) → Fin (d j + 1)) => P.coeff (boxMonomial d I)) = P

A polynomial whose partial degrees are bounded by d is the polynomial of its own coefficient vector on the box.

theorem MvPolynomial.ofBox_injective {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} : Function.Injective ⇑(ofBox d)

theorem MvPolynomial.range_ofBox {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {d : σ → ℕ} : (ofBox d).range = restrictSupport R {ν : σ →₀ ℕ | ∀ (j : σ), ν j ≤ d j}

The polynomials with a coefficient vector on the box are exactly the polynomials supported in the box.

The vanishing conditions as linear forms

def MvPolynomial.hasseDerivRow {σ : Type u_1} {S : Type u_2} [Fintype σ] [CommSemiring S] (d : σ → ℕ) (α : σ → S) (μ : σ →₀ ℕ) (I : (j : σ) → Fin (d j + 1)) : S

The row of the linear condition "∂^μ P vanishes at α" on the coefficient vector of a polynomial P of the box: its entry at the exponent I is ∏ j, (I j choose μ j) α j ^ (I j - μ j).

theorem MvPolynomial.hasseDerivRow_def {σ : Type u_1} {S : Type u_2} [Fintype σ] [CommSemiring S] (d : σ → ℕ) (α : σ → S) (μ : σ →₀ ℕ) (I : (j : σ) → Fin (d j + 1)) : hasseDerivRow d α μ I = ∏ j : σ, ↑((↑(I j)).choose (μ j)) * α j ^ (↑(I j) - μ j)

@[simp]

theorem MvPolynomial.hasseDerivRow_zero {σ : Type u_1} {S : Type u_2} [Fintype σ] [CommSemiring S] (d : σ → ℕ) (α : σ → S) (I : (j : σ) → Fin (d j + 1)) : hasseDerivRow d α 0 I = ∏ j : σ, α j ^ ↑(I j)

The row of order 0 is the tuple of the monomials of the box at α: the condition of order 0 is the vanishing of P at α.

theorem MvPolynomial.hasseDerivRow_eq_zero {σ : Type u_1} {S : Type u_2} [Fintype σ] [CommSemiring S] {d : σ → ℕ} (α : σ → S) {μ : σ →₀ ℕ} {j : σ} (hj : d j < μ j) : hasseDerivRow d α μ = 0

An order that leaves the box in some variable has the zero row.

theorem MvPolynomial.aeval_hasseDeriv_ofBox {σ : Type u_1} {S : Type u_2} [Fintype σ] [CommSemiring S] [DecidableEq σ] {R : Type u_3} [CommSemiring R] [Algebra R S] {d : σ → ℕ} (x : ((j : σ) → Fin (d j + 1)) → R) (α : σ → S) (μ : σ →₀ ℕ) : (aeval α) ((hasseDeriv μ) ((ofBox d) x)) = ∑ I : (j : σ) → Fin (d j + 1), hasseDerivRow d α μ I * (algebraMap R S) (x I)

The value at α of a Hasse derivative of the polynomial with coefficient vector x on the box is the row hasseDerivRow d α μ applied to x.

theorem MvPolynomial.aeval_hasseDeriv_eq_sum {σ : Type u_1} {S : Type u_2} [Fintype σ] [CommSemiring S] [DecidableEq σ] {R : Type u_3} [CommSemiring R] [Algebra R S] {d : σ → ℕ} {P : MvPolynomial σ R} (hP : ∀ (j : σ), degreeOf j P ≤ d j) (α : σ → S) (μ : σ →₀ ℕ) : (aeval α) ((hasseDeriv μ) P) = ∑ I : (j : σ) → Fin (d j + 1), hasseDerivRow d α μ I * (algebraMap R S) (P.coeff (boxMonomial d I))

The value at α of a Hasse derivative of a polynomial whose partial degrees are bounded by d is the row hasseDerivRow d α μ applied to its coefficient vector on the box.

Examples