Projective coefficient heights of multivariate polynomials

The height of a multivariate polynomial is the native projective height of its finitely supported coefficient vector. The variables may form an infinite type: only the finitely many nonzero coefficients contribute. Nonzero scalar multiplication, injective variable renaming, and placement of a univariate polynomial in one coordinate preserve the height. These comparisons allow auxiliary polynomials to be handled in their natural variable types.

The normalization is relative to the admissible family of absolute values of the field. In particular, constant polynomials and the zero polynomial have multiplicative height one. For polynomials over number fields, logHeight_eq_of_numberField expresses the height as a sum of local logarithmic sup norms, with complex-place multiplicity two.

There is no bound for the height of a sum of polynomials in terms of the heights of its terms, so the height of a determinant of a matrix of polynomials is bounded place by place. Matrix.mulHeight_det_le and Matrix.logHeight_det_le do this for an n × n matrix whose entries have partial degrees at most d j and coefficients dominated by those of one polynomial P, up to a factor C at the archimedean absolute values: h(det A) ≤ n h(P) + totalWeight K * (log n! + n (∑ j, d j * log 2 + log C)). This applies to the generalized Wronskians of Hasse derivatives of P in Roth's lemma: MvPolynomial.logHeight_det_hasseDeriv_le bounds the height of any n × n determinant of Hasse derivatives of P by n h(P) + totalWeight K * (log n! + 2 n ∑ j, d j * log 2).

Although the height of a product is not the product of the heights in general, it is when the two factors involve disjoint sets of variables: then the coefficients of the product are exactly the products of the coefficients of the factors. mulHeight_mul_of_disjoint_vars and logHeight_mul_of_disjoint_vars state H(P Q) = H(P) H(Q) and h(P Q) = h(P) + h(Q) for nonzero P and Q, and mulHeight_mul_toMvPolynomial specializes them to a product of a polynomial not involving Xᵢ with a one-variable polynomial placed in Xᵢ. In the inductive step of Roth's lemma, this is the shape of the product of a generalized Wronskian and a one-variable Wronskian.

For a polynomial whose partial degrees are bounded by d, the height is the height of its coefficient vector on the box ∀ j, Fin (d j + 1) (MvPolynomial.mulHeight_ofBox). The vanishing of a Hasse derivative at a point α is a linear condition on that vector with row MvPolynomial.hasseDerivRow d α μ, and MvPolynomial.mulHeight_hasseDerivRow_le bounds the height of the row by (2 ^ ∑ j, d j) ^ totalWeight K * ∏ j, mulHeight₁ (α j) ^ d j. These are the heights that Siegel's lemma charges when it produces a polynomial of prescribed index at given points.

References

• Lukas Pottmeyer, Diophantine Approximation, §3.2, Definition 3.2.1 and Lemma 3.2.2 (17 January 2022). The absolute heights in those notes correspond to degree-root normalizations of the relative heights defined here. The determinant bound is the estimate of §3.4.6. The height of a product in disjoint variables is Exercise 3.3.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Proposition 1.6.2.
• The determinant bound follows DiophantineApproximation/PolynomialDeterminantHeight.lean in Ralf Stephan's rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0). The height of a product in disjoint variables adapts DiophantineApproximation/DisjointVariables.lean of the same snapshot. The heights of coefficient vectors on the box and of the rows of the vanishing conditions follow DiophantineApproximation/BoxMonomial.lean and DiophantineApproximation/MonomialHeight.lean of the same repository, commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338; the row bound there assumes the order lies in the box, which is not needed here. See also Bombieri–Gubler, Lemma 6.3.4.

noncomputable def MvPolynomial.mulHeight {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : ℝ

The relative projective multiplicative height of a multivariate coefficient vector.

noncomputable def MvPolynomial.logHeight {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : ℝ

The relative projective logarithmic height of a multivariate coefficient vector.

theorem MvPolynomial.mulHeight_eq_finsupp {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : p.mulHeight = p.coeff.mulHeight

theorem MvPolynomial.logHeight_eq_log_mulHeight {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : p.logHeight = Real.log p.mulHeight

theorem MvPolynomial.logHeight_eq_finsupp {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : p.logHeight = p.coeff.logHeight

Multivariate logarithmic height agrees with the native finitely supported height.

theorem MvPolynomial.mulHeight_eq_support {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : p.mulHeight = Height.mulHeight fun (i : ↥p.support) => p.coeff ↑i

Multivariate height is the height of the tuple indexed by its nonzero coefficients.

theorem MvPolynomial.mulHeight_eq_coeff {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) (s : Finset (σ →₀ ℕ)) (hs : p.support ⊆ s) : p.mulHeight = Height.mulHeight fun (i : ↥s) => p.coeff ↑i

Padding a finite coefficient tuple with zeroes does not change multivariate height.

theorem MvPolynomial.logHeight_eq_coeff {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) (s : Finset (σ →₀ ℕ)) (hs : p.support ⊆ s) : p.logHeight = Height.logHeight fun (i : ↥s) => p.coeff ↑i

The logarithmic height of any finite coefficient tuple containing the support.

theorem MvPolynomial.one_le_mulHeight {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : 1 ≤ p.mulHeight

theorem MvPolynomial.mulHeight_pos {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : 0 < p.mulHeight

theorem MvPolynomial.logHeight_nonneg {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : 0 ≤ p.logHeight

@[simp]

theorem MvPolynomial.mulHeight_zero {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] : mulHeight 0 = 1

@[simp]

theorem MvPolynomial.logHeight_zero {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] : logHeight 0 = 0

@[simp]

theorem MvPolynomial.mulHeight_monomial {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (n : σ →₀ ℕ) (c : K) : ((monomial n) c).mulHeight = 1

@[simp]

theorem MvPolynomial.logHeight_monomial {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (n : σ →₀ ℕ) (c : K) : ((monomial n) c).logHeight = 0

@[simp]

theorem MvPolynomial.mulHeight_C {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (c : K) : (C c).mulHeight = 1

@[simp]

theorem MvPolynomial.logHeight_C {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (c : K) : (C c).logHeight = 0

@[simp]

theorem MvPolynomial.mulHeight_one {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] : mulHeight 1 = 1

@[simp]

theorem MvPolynomial.logHeight_one {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] : logHeight 1 = 0

@[simp]

theorem MvPolynomial.mulHeight_X_pow {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : σ) (n : ℕ) : (X i ^ n).mulHeight = 1

@[simp]

theorem MvPolynomial.logHeight_X_pow {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : σ) (n : ℕ) : (X i ^ n).logHeight = 0

@[simp]

theorem MvPolynomial.mulHeight_X {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : σ) : (X i).mulHeight = 1

@[simp]

theorem MvPolynomial.logHeight_X {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : σ) : (X i).logHeight = 0

@[simp]

theorem MvPolynomial.mulHeight_smul {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) {c : K} (hc : c ≠ 0) : (c • p).mulHeight = p.mulHeight

Nonzero scalar multiplication does not change multivariate coefficient height.

@[simp]

theorem MvPolynomial.mulHeight_C_mul {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) {c : K} (hc : c ≠ 0) : (C c * p).mulHeight = p.mulHeight

@[simp]

theorem MvPolynomial.logHeight_smul {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) {c : K} (hc : c ≠ 0) : (c • p).logHeight = p.logHeight

@[simp]

theorem MvPolynomial.mulHeight_neg {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : (-p).mulHeight = p.mulHeight

@[simp]

theorem MvPolynomial.logHeight_neg {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) : (-p).logHeight = p.logHeight

@[simp]

theorem MvPolynomial.logHeight_C_mul {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) {c : K} (hc : c ≠ 0) : (C c * p).logHeight = p.logHeight

@[simp]

theorem MvPolynomial.mulHeight_rename {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) {f : σ → τ} (hf : Function.Injective f) : ((rename f) p).mulHeight = p.mulHeight

Injective renaming of variables preserves projective coefficient height.

@[simp]

theorem MvPolynomial.logHeight_rename {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] [Height.AdmissibleAbsValues K] (p : MvPolynomial σ K) {f : σ → τ} (hf : Function.Injective f) : ((rename f) p).logHeight = p.logHeight

@[simp]

theorem Polynomial.mulHeight_toMvPolynomial {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) (i : σ) : ((toMvPolynomial i) p).mulHeight = p.mulHeight

Placement in a multivariate coordinate preserves projective coefficient height.

@[simp]

theorem Polynomial.logHeight_toMvPolynomial {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (p : Polynomial K) (i : σ) : ((toMvPolynomial i) p).logHeight = p.logHeight

@[simp]

theorem MvPolynomial.mulHeight_X_sub_C {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : σ) (a : K) : (X i - C a).mulHeight = Height.mulHeight₁ a

The coefficient height of X i - C a is the scalar multiplicative height of a.

@[simp]

theorem MvPolynomial.logHeight_X_sub_C {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : σ) (a : K) : (X i - C a).logHeight = Height.logHeight₁ a

The coefficient height of X i - C a is the scalar logarithmic height of a.

theorem MvPolynomial.mulHeight_mul_of_disjoint_vars {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] {P Q : MvPolynomial σ K} (h : Disjoint P.vars Q.vars) (hP : P ≠ 0) (hQ : Q ≠ 0) : (P * Q).mulHeight = P.mulHeight * Q.mulHeight

The height of a product in disjoint variables. If the nonzero polynomials P and Q involve disjoint sets of variables, then H(P * Q) = H(P) H(Q). In general the height of a product is only bounded by the product of the heights up to a factor depending on the degrees.

theorem MvPolynomial.logHeight_mul_of_disjoint_vars {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] {P Q : MvPolynomial σ K} (h : Disjoint P.vars Q.vars) (hP : P ≠ 0) (hQ : Q ≠ 0) : (P * Q).logHeight = P.logHeight + Q.logHeight

The logarithmic height of a product in disjoint variables. If the nonzero polynomials P and Q involve disjoint sets of variables, then h(P * Q) = h(P) + h(Q).

theorem MvPolynomial.mulHeight_mul_toMvPolynomial {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] {F : MvPolynomial σ K} {i : σ} (hi : i ∉ F.vars) (hF : F ≠ 0) {p : Polynomial K} (hp : p ≠ 0) : (F * (Polynomial.toMvPolynomial i) p).mulHeight = F.mulHeight * p.mulHeight

If the nonzero polynomial F does not involve the variable Xᵢ, then multiplying it by a nonzero one-variable polynomial p placed in Xᵢ multiplies its height by the height of p.

theorem MvPolynomial.logHeight_mul_toMvPolynomial {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] {F : MvPolynomial σ K} {i : σ} (hi : i ∉ F.vars) (hF : F ≠ 0) {p : Polynomial K} (hp : p ≠ 0) : (F * (Polynomial.toMvPolynomial i) p).logHeight = F.logHeight + p.logHeight

If the nonzero polynomial F does not involve the variable Xᵢ, then multiplying it by a nonzero one-variable polynomial p placed in Xᵢ adds the logarithmic height of p.

theorem MvPolynomial.logHeight_eq_of_numberField {K : Type u_1} {σ : Type u_2} [Field K] [NumberField K] (p : MvPolynomial σ K) : p.logHeight = ∑ v : NumberField.InfinitePlace K, ↑v.mult * Real.log (⨆ (d : σ →₀ ℕ), v (p.coeff d)) + ∑ᶠ (v : NumberField.FinitePlace K), Real.log (⨆ (d : σ →₀ ℕ), v (p.coeff d))

Over a number field, the relative logarithmic coefficient height is the sum of local logarithmic sup norms. Infinite places occur with their real or complex multiplicity; divide by [K : ℚ] for the absolute normalization. The variables may form an infinite type.

theorem Matrix.mulHeight_det_le {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n (MvPolynomial σ K)) {P : MvPolynomial σ K} {d : σ → ℕ} (hd : ∀ (i j : n) (k : σ), MvPolynomial.degreeOf k (A i j) ≤ d k) {C : ℝ} (hC : 1 ≤ C) (harch : ∀ v ∈ Height.AdmissibleAbsValues.archAbsVal, ∀ (i j : n) (a : σ →₀ ℕ), ∃ (b : σ →₀ ℕ), v ((A i j).coeff a) ≤ C * v (P.coeff b)) (hnon : ∀ v ∈ Height.AdmissibleAbsValues.nonarchAbsVal, ∀ (i j : n) (a : σ →₀ ℕ), ∃ (b : σ →₀ ℕ), v ((A i j).coeff a) ≤ v (P.coeff b)) : A.det.mulHeight ≤ (↑(Fintype.card n).factorial * ((2 ^ ∑ k : σ, d k) * C) ^ Fintype.card n) ^ Height.totalWeight K * P.mulHeight ^ Fintype.card n

The height of a determinant of polynomials. Let A be an n × n matrix of polynomials whose entries have partial degrees at most d j, and let P be a polynomial. Suppose that, at every archimedean absolute value v, each coefficient of each entry is bounded by C times v of some coefficient of P, and at every nonarchimedean v by v of some coefficient of P. Then H(det A) ≤ (n! (2 ^ (∑ j, d j) * C) ^ n) ^ totalWeight K * H(P) ^ n.

theorem Matrix.logHeight_det_le {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n (MvPolynomial σ K)) {P : MvPolynomial σ K} {d : σ → ℕ} (hd : ∀ (i j : n) (k : σ), MvPolynomial.degreeOf k (A i j) ≤ d k) {C : ℝ} (hC : 1 ≤ C) (harch : ∀ v ∈ Height.AdmissibleAbsValues.archAbsVal, ∀ (i j : n) (a : σ →₀ ℕ), ∃ (b : σ →₀ ℕ), v ((A i j).coeff a) ≤ C * v (P.coeff b)) (hnon : ∀ v ∈ Height.AdmissibleAbsValues.nonarchAbsVal, ∀ (i j : n) (a : σ →₀ ℕ), ∃ (b : σ →₀ ℕ), v ((A i j).coeff a) ≤ v (P.coeff b)) : A.det.logHeight ≤ ↑(Fintype.card n) * P.logHeight + ↑(Height.totalWeight K) * (Real.log ↑(Fintype.card n).factorial + ↑(Fintype.card n) * (∑ k : σ, ↑(d k) * Real.log 2 + Real.log C))

The logarithmic height of a determinant of polynomials. Under the hypotheses of Matrix.mulHeight_det_le, h(det A) ≤ n h(P) + totalWeight K * (log n! + n (∑ j, d j * log 2 + log C)).

theorem MvPolynomial.logHeight_det_hasseDeriv_le {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] {n : Type u_3} [Fintype n] [DecidableEq n] {P : MvPolynomial σ K} {d : σ → ℕ} (hd : ∀ (j : σ), degreeOf j P ≤ d j) (E : n → n → σ →₀ ℕ) : (Matrix.of fun (k l : n) => (hasseDeriv (E k l)) P).det.logHeight ≤ ↑(Fintype.card n) * P.logHeight + ↑(Height.totalWeight K) * (Real.log ↑(Fintype.card n).factorial + 2 * ↑(Fintype.card n) * ∑ j : σ, ↑(d j) * Real.log 2)

The height of a determinant of Hasse derivatives (Pottmeyer, §3.4.6). If P has partial degrees at most d j, then any n × n determinant of Hasse derivatives ∂^(E k l) P has height h(det) ≤ n h(P) + totalWeight K * (log n! + 2 n ∑ j, d j * log 2).

Polynomials of bounded partial degrees and the rows of their vanishing conditions

@[simp]

theorem MvPolynomial.mulHeight_ofBox {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] {d : σ → ℕ} [DecidableEq σ] (x : ((j : σ) → Fin (d j + 1)) → K) : ((ofBox d) x).mulHeight = Height.mulHeight x

The height of the polynomial with coefficient vector x on the box ∀ j, Fin (d j + 1) is the height of x.

@[simp]

theorem MvPolynomial.logHeight_ofBox {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] {d : σ → ℕ} [DecidableEq σ] (x : ((j : σ) → Fin (d j + 1)) → K) : ((ofBox d) x).logHeight = Height.logHeight x

The logarithmic height of the polynomial with coefficient vector x on the box is the logarithmic height of x.

theorem MvPolynomial.mulHeight_hasseDerivRow_le {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] (d : σ → ℕ) (α : σ → K) (μ : σ →₀ ℕ) : Height.mulHeight (hasseDerivRow d α μ) ≤ (2 ^ ∑ j : σ, d j) ^ Height.totalWeight K * ∏ j : σ, Height.mulHeight₁ (α j) ^ d j

The height of a row of the vanishing conditions on the box ∀ j, Fin (d j + 1) at the point α is at most (2 ^ ∑ j, d j) ^ totalWeight K * ∏ j, mulHeight₁ (α j) ^ d j. The order μ need not lie in the box: outside it the row is zero.

theorem MvPolynomial.logHeight_hasseDerivRow_le {K : Type u_1} {σ : Type u_2} [Field K] [Height.AdmissibleAbsValues K] [Fintype σ] (d : σ → ℕ) (α : σ → K) (μ : σ →₀ ℕ) : Height.logHeight (hasseDerivRow d α μ) ≤ ↑(Height.totalWeight K) * ↑(∑ j : σ, d j) * Real.log 2 + ∑ j : σ, ↑(d j) * Height.logHeight₁ (α j)

The logarithmic height of a row of the vanishing conditions on the box at the point α is at most totalWeight K * (∑ j, d j) * log 2 + ∑ j, d j * logHeight₁ (α j).