Generalized Wronskians of multivariate polynomials

For a family f : Fin m → MvPolynomial σ R and a family of multi-indices D : Fin m → σ →₀ ℕ, the generalized Wronskian W_D(f) is the determinant det (∂^(D k) f_l) of the m × m matrix whose (k, l) entry is the D k-th Hasse derivative of f_l. The row family is admissible when |D k| ≤ k for every k; admissibility is a hypothesis of the theorems, not part of the definition. With the rows D k = k eᵢ and a family of polynomials in the single variable Xᵢ, the generalized Wronskian is the one-variable Hasse Wronskian Polynomial.hasseWronskian.

Over an integral domain a linearly dependent family has vanishing generalized Wronskians for every row family. Over a field of characteristic zero the converse holds in the following form: a linearly independent family has a nonzero generalized Wronskian with admissible rows. Generalized Wronskians are the auxiliary determinants of Roth's lemma, which bounds the index of a polynomial in several variables at a point; admissibility controls their degrees.

Main definitions

• MvPolynomial.genWronskian D f: the determinant of the Hasse derivatives ∂^(D k) f_l.

Main results

• MvPolynomial.map_genWronskian, MvPolynomial.eval_genWronskian: generalized Wronskians commute with maps of coefficient rings and with evaluation.
• MvPolynomial.genWronskian_single_toMvPolynomial: in a single variable, with rows k eᵢ, the generalized Wronskian is the Hasse Wronskian.
• MvPolynomial.genWronskian_eq_zero_of_not_linearIndependent: over an integral domain, dependent families have vanishing generalized Wronskians.
• MvPolynomial.det_hasseDeriv_sum_mul_toMvPolynomial: for P = ∑ₖ fₖ · gₖ(Xᵢ) with the fₖ free of Xᵢ and rows D k that do not differentiate in Xᵢ (D k i = 0 for every k), the determinant det (∂^(D k + l eᵢ) P) is the product of the generalized Wronskian of the fₖ and the Hasse Wronskian of the gₖ.
• MvPolynomial.linearIndependent_iff_exists_genWronskian_ne_zero: over a field of characteristic zero, a family is linearly independent if and only if some admissible generalized Wronskian is nonzero.

Implementation notes

The nonvanishing direction reduces to one variable. The Kronecker substitution Xₛ ↦ T ^ eₛ, for a weight e separating the exponents of the family, preserves linear independence, so the image family has a nonzero Hasse Wronskian, which survives evaluation at some point a. Translating T to a + U turns the substitution into Xₛ ↦ (U + a) ^ eₛ - a ^ eₛ, whose images have no constant term. Hence the k-th Hasse derivative of an image, evaluated at a, is a linear combination of Hasse derivatives ∂^ν f of total order |ν| ≤ k, evaluated at (a ^ eₛ)ₛ. Expanding the determinant multilinearly in its rows exhibits a nonzero admissible generalized Wronskian.

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (version of 17 January 2022), §3.3: Definition 3.3.5, Theorem 3.3.7 and Lemma 3.3.9.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Proposition 6.3.10, whose proof by Kronecker substitution is followed here.
• The proof plan (separating weights, translated substitution and multilinear expansion of the determinant) is adapted from Ralf Stephan's DiophantineApproximation/GeneralizedWronskian.lean in rwst/Subspace-Theorems, commit 5cff93ceb4b69b2048473301411763febe96bb3f (Apache 2.0).

noncomputable def MvPolynomial.genWronskian {R : Type u_1} {σ : Type u_3} [CommRing R] {m : ℕ} (D : Fin m → σ →₀ ℕ) (f : Fin m → MvPolynomial σ R) : MvPolynomial σ R

The generalized Wronskian W_D(f) of a family f : Fin m → MvPolynomial σ R with respect to the row family D : Fin m → σ →₀ ℕ: the determinant of the matrix whose (k, l) entry is the Hasse derivative ∂^(D k) f_l. The generalized Wronskian of the empty family is 1.

theorem MvPolynomial.genWronskian_def {R : Type u_1} {σ : Type u_3} [CommRing R] {m : ℕ} (D : Fin m → σ →₀ ℕ) (f : Fin m → MvPolynomial σ R) : genWronskian D f = (Matrix.of fun (k l : Fin m) => (hasseDeriv (D k)) (f l)).det

The generalized Wronskian is the determinant of the matrix of Hasse derivatives ∂^(D k) f_l.

@[simp]

theorem MvPolynomial.genWronskian_fin_zero {R : Type u_1} {σ : Type u_3} [CommRing R] (D : Fin 0 → σ →₀ ℕ) (f : Fin 0 → MvPolynomial σ R) : genWronskian D f = 1

The generalized Wronskian of the empty family is 1.

@[simp]

theorem MvPolynomial.genWronskian_fin_one {R : Type u_1} {σ : Type u_3} [CommRing R] (D : Fin 1 → σ →₀ ℕ) (f : Fin 1 → MvPolynomial σ R) : genWronskian D f = (hasseDeriv (D 0)) (f 0)

The generalized Wronskian of a single polynomial f₀ is ∂^(D 0) f₀; for the admissible row D 0 = 0 it is f₀.

@[simp]

theorem MvPolynomial.map_genWronskian {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommRing R] [CommRing S] {m : ℕ} (g : R →+* S) (D : Fin m → σ →₀ ℕ) (f : Fin m → MvPolynomial σ R) : (map g) (genWronskian D f) = genWronskian D fun (l : Fin m) => (map g) (f l)

Generalized Wronskians commute with maps of coefficient rings.

theorem MvPolynomial.eval_genWronskian {R : Type u_1} {σ : Type u_3} [CommRing R] {m : ℕ} (x : σ → R) (D : Fin m → σ →₀ ℕ) (f : Fin m → MvPolynomial σ R) : (eval x) (genWronskian D f) = (Matrix.of fun (k l : Fin m) => (eval x) ((hasseDeriv (D k)) (f l))).det

Evaluating a generalized Wronskian at x gives the determinant of the values of the Hasse derivatives ∂^(D k) f_l at x.

@[simp]

theorem MvPolynomial.genWronskian_single_toMvPolynomial {R : Type u_1} {σ : Type u_3} [CommRing R] {m : ℕ} (i : σ) (g : Fin m → Polynomial R) : (genWronskian (fun (k : Fin m) => Finsupp.single i ↑k) fun (l : Fin m) => (Polynomial.toMvPolynomial i) (g l)) = (Polynomial.toMvPolynomial i) (Polynomial.hasseWronskian g)

In the single variable Xᵢ, with rows D k = k eᵢ, the generalized Wronskian is the one-variable Hasse Wronskian.

theorem MvPolynomial.genWronskian_eq_zero_of_not_linearIndependent {R : Type u_1} {σ : Type u_3} [CommRing R] {m : ℕ} [IsDomain R] (D : Fin m → σ →₀ ℕ) {f : Fin m → MvPolynomial σ R} (hf : ¬LinearIndependent R f) : genWronskian D f = 0

Over an integral domain, every generalized Wronskian of a linearly dependent family vanishes. No row admissibility or characteristic assumption is needed.

theorem MvPolynomial.det_hasseDeriv_sum_mul_toMvPolynomial {R : Type u_1} {σ : Type u_3} [CommRing R] {m : ℕ} {i : σ} {D : Fin m → σ →₀ ℕ} (hD : ∀ (k : Fin m), (D k) i = 0) {f : Fin m → MvPolynomial σ R} (hf : ∀ (k : Fin m), i ∉ (f k).vars) (g : Fin m → Polynomial R) : (Matrix.of fun (k l : Fin m) => (hasseDeriv (D k + Finsupp.single i ↑l)) (∑ j : Fin m, f j * (Polynomial.toMvPolynomial i) (g j))).det = genWronskian D f * (Polynomial.toMvPolynomial i) (Polynomial.hasseWronskian g)

Separation of variables for generalized Wronskians (Pottmeyer, Lemma 3.3.9). Let P = ∑ₖ fₖ · gₖ(Xᵢ), where no fₖ involves Xᵢ, and let the rows D k not differentiate in Xᵢ. Then the determinant of the Hasse derivatives ∂^(D k + l eᵢ) P is the product of the generalized Wronskian W_D(f) and the Hasse Wronskian of the gₖ, placed in Xᵢ.

The generalized Wronskian criterion

theorem MvPolynomial.exists_genWronskian_ne_zero {σ : Type u_3} {m : ℕ} {K : Type u_4} [Field K] [CharZero K] {f : Fin m → MvPolynomial σ K} (hf : LinearIndependent K f) : ∃ (D : Fin m → σ →₀ ℕ), (∀ (k : Fin m), Finsupp.degree (D k) ≤ ↑k) ∧ genWronskian D f ≠ 0

Over a field of characteristic zero, a linearly independent family of polynomials has a nonzero generalized Wronskian with admissible rows |D k| ≤ k.

theorem MvPolynomial.linearIndependent_iff_exists_genWronskian_ne_zero {σ : Type u_3} {m : ℕ} {K : Type u_4} [Field K] [CharZero K] {f : Fin m → MvPolynomial σ K} : LinearIndependent K f ↔ ∃ (D : Fin m → σ →₀ ℕ), (∀ (k : Fin m), Finsupp.degree (D k) ≤ ↑k) ∧ genWronskian D f ≠ 0

The generalized Wronskian criterion. Over a field of characteristic zero, a family of multivariate polynomials is linearly independent if and only if some generalized Wronskian with admissible rows |D k| ≤ k is nonzero.