Partial-degree bounds for generalized Wronskians

The generalized Wronskian of m multivariate polynomials is an m × m determinant whose entries are Hasse derivatives. Since Hasse derivatives do not increase partial degree, its partial degree in any variable is at most the sum of the corresponding partial-degree bounds for the columns. In particular, a common bound N on the columns gives the bound m * N.

This is the degree estimate used for the auxiliary generalized Wronskians in Roth's lemma.

Main results

• MvPolynomial.degreeOf_genWronskian_le_sum: bounds a generalized Wronskian using a separate partial-degree bound for every column.
• MvPolynomial.degreeOf_genWronskian_le: a common partial-degree bound N gives the bound m * N.
• MvPolynomial.notMem_vars_genWronskian, MvPolynomial.eq_zero_of_genWronskian_ne_zero: a variable that no column involves does not occur in a generalized Wronskian, and a nonzero one has no row differentiating in it.

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (version of 17 January 2022), §3.4.5.

theorem MvPolynomial.degreeOf_genWronskian_le_sum {R : Type u_1} {σ : Type u_2} [CommRing R] {m : ℕ} (D : Fin m → σ →₀ ℕ) (f : Fin m → MvPolynomial σ R) (i : σ) (e : Fin m → ℕ) (hf : ∀ (l : Fin m), degreeOf i (f l) ≤ e l) : degreeOf i (genWronskian D f) ≤ ∑ l : Fin m, e l

If the l-th polynomial has partial degree at most e l in Xᵢ, then the partial degree of any generalized Wronskian of the family in Xᵢ is at most ∑ l, e l.

No admissibility hypothesis on the derivative rows is needed: every Hasse derivative weakly decreases each partial degree.

theorem MvPolynomial.degreeOf_genWronskian_le {R : Type u_1} {σ : Type u_2} [CommRing R] {m : ℕ} (D : Fin m → σ →₀ ℕ) (f : Fin m → MvPolynomial σ R) (i : σ) (N : ℕ) (hf : ∀ (l : Fin m), degreeOf i (f l) ≤ N) : degreeOf i (genWronskian D f) ≤ m * N

If every polynomial in a family of size m has partial degree at most N in Xᵢ, then the partial degree of any generalized Wronskian of the family in Xᵢ is at most m * N.

theorem MvPolynomial.notMem_vars_genWronskian {R : Type u_1} {σ : Type u_2} [CommRing R] {m : ℕ} {i : σ} {f : Fin m → MvPolynomial σ R} (hf : ∀ (l : Fin m), i ∉ (f l).vars) (D : Fin m → σ →₀ ℕ) : i ∉ (genWronskian D f).vars

A generalized Wronskian of polynomials that do not involve Xᵢ does not involve Xᵢ.

theorem MvPolynomial.eq_zero_of_genWronskian_ne_zero {R : Type u_1} {σ : Type u_2} [CommRing R] {m : ℕ} {i : σ} {D : Fin m → σ →₀ ℕ} {f : Fin m → MvPolynomial σ R} (hf : ∀ (l : Fin m), i ∉ (f l).vars) (hW : genWronskian D f ≠ 0) (k : Fin m) : (D k) i = 0

If no polynomial of the family involves Xᵢ and the generalized Wronskian is nonzero, then no row differentiates in Xᵢ: each Hasse derivative in a row differentiating in Xᵢ vanishes.