The Wronskian of a family of polynomials built from Hasse derivatives

For a family g : Fin m → R[X] of one-variable polynomials over a commutative ring, the Hasse Wronskian is the determinant det (Dᵏ gₗ) of the m × m matrix whose (k, l) entry is the k-th Hasse (divided) derivative of gₗ; the rows are the derivative orders 0 ≤ k < m and the columns are the members of the family. Multiplying it by ∏ k < m, k! gives the classical Wronskian det (gₗ⁽ᵏ⁾), the Derivation.wronskian of the derivation derivative', but the divided version has the advantage of being defined and integral over any commutative ring. Mathlib's Polynomial.wronskian is the case of two polynomials.

Over an integral domain a linearly dependent family has vanishing Hasse Wronskian. Over a field of characteristic zero the converse holds, so linear independence is equivalent to nonvanishing of the Hasse Wronskian. In positive characteristic the converse fails: over 𝔽₂ the polynomials 1 and X² are independent, but D¹ (X²) = 2X = 0.

This is the one-variable Wronskian used in the proof of Roth's lemma on the index of auxiliary polynomials.

Main definitions

• Polynomial.hasseWronskian g: the determinant of the Hasse derivatives Dᵏ gₗ, k, l < m.

Main results

• Polynomial.hasseWronskian_fin_two: for two polynomials it is Mathlib's wronskian.
• Polynomial.prod_factorial_mul_hasseWronskian: (∏ k, k!) W(g) is the classical Wronskian derivative'.wronskian g.
• Polynomial.hasseWronskian_comp_perm: permuting the family multiplies W(g) by the sign.
• Polynomial.hasseWronskian_map: W(g) commutes with maps of coefficient rings.
• Polynomial.hasseWronskian_eq_zero_of_not_linearIndependent: over an integral domain, dependent families have vanishing Hasse Wronskian.
• Polynomial.linearIndependent_iff_hasseWronskian_ne_zero: over a field of characteristic zero, a family is linearly independent if and only if its Hasse Wronskian is nonzero.

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (version of 17 January 2022), §3.3: Definition 3.3.1, Lemma 3.3.2, Proposition 3.3.3 and Remark 3.3.6.

noncomputable def Polynomial.hasseWronskian {R : Type u_1} [CommRing R] {m : ℕ} (g : Fin m → Polynomial R) : Polynomial R

The Hasse Wronskian of a family g : Fin m → R[X] of polynomials: the determinant of the matrix whose (k, l) entry is the k-th Hasse derivative Dᵏ gₗ of the l-th polynomial. The Hasse Wronskian of the empty family is 1.

theorem Polynomial.hasseWronskian_def {R : Type u_1} [CommRing R] {m : ℕ} (g : Fin m → Polynomial R) : hasseWronskian g = (Matrix.of fun (k l : Fin m) => (hasseDeriv ↑k) (g l)).det

The Hasse Wronskian is the determinant of the matrix of Hasse derivatives Dᵏ gₗ.

@[simp]

theorem Polynomial.hasseWronskian_fin_zero {R : Type u_1} [CommRing R] (g : Fin 0 → Polynomial R) : hasseWronskian g = 1

The Hasse Wronskian of the empty family is 1.

@[simp]

theorem Polynomial.hasseWronskian_fin_one {R : Type u_1} [CommRing R] (g : Fin 1 → Polynomial R) : hasseWronskian g = g 0

The Hasse Wronskian of a single polynomial is that polynomial.

@[simp]

theorem Polynomial.hasseWronskian_fin_two {R : Type u_1} [CommRing R] (g : Fin 2 → Polynomial R) : hasseWronskian g = (g 0).wronskian (g 1)

The Hasse Wronskian of two polynomials is Mathlib's Wronskian g₀ g₁' - g₀' g₁.

theorem Polynomial.prod_factorial_mul_hasseWronskian {R : Type u_1} [CommRing R] {m : ℕ} (g : Fin m → Polynomial R) : (∏ k : Fin m, ↑(↑k).factorial) * hasseWronskian g = derivative'.wronskian g

Multiplying the Hasse Wronskian by ∏ k < m, k! gives the classical Wronskian, the determinant of the iterated ordinary derivatives derivative^[k] gₗ.

theorem Polynomial.hasseWronskian_comp_perm {R : Type u_1} [CommRing R] {m : ℕ} (g : Fin m → Polynomial R) (σ : Equiv.Perm (Fin m)) : hasseWronskian (g ∘ ⇑σ) = ↑↑(Equiv.Perm.sign σ) * hasseWronskian g

Permuting the family multiplies the Hasse Wronskian by the sign of the permutation.

@[simp]

theorem Polynomial.hasseWronskian_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {m : ℕ} (f : R →+* S) (g : Fin m → Polynomial R) : (hasseWronskian fun (l : Fin m) => map f (g l)) = map f (hasseWronskian g)

The Hasse Wronskian commutes with maps of coefficient rings.

theorem Polynomial.hasseWronskian_update_add_smul {R : Type u_1} [CommRing R] {m : ℕ} (g : Fin m → Polynomial R) {i j : Fin m} (hij : i ≠ j) (a : R) : hasseWronskian (Function.update g j (g j + a • g i)) = hasseWronskian g

Adding a multiple of one member of the family to another does not change the Hasse Wronskian.

theorem Polynomial.hasseWronskian_eq_zero_of_not_linearIndependent {R : Type u_1} [CommRing R] {m : ℕ} [IsDomain R] {g : Fin m → Polynomial R} (hg : ¬LinearIndependent R g) : hasseWronskian g = 0

Over an integral domain, the Hasse Wronskian of a linearly dependent family vanishes.

theorem Polynomial.hasseWronskian_ne_zero_of_injective_natDegree {R : Type u_1} [CommRing R] {m : ℕ} [IsDomain R] [CharZero R] {g : Fin m → Polynomial R} (hg : ∀ (l : Fin m), g l ≠ 0) (hinj : Function.Injective fun (l : Fin m) => (g l).natDegree) : hasseWronskian g ≠ 0

Over a domain of characteristic zero, a family of nonzero polynomials of pairwise distinct degrees has nonzero Hasse Wronskian.

theorem Polynomial.hasseWronskian_ne_zero_of_linearIndependent {m : ℕ} {K : Type u_3} [Field K] [CharZero K] {g : Fin m → Polynomial K} (hg : LinearIndependent K g) : hasseWronskian g ≠ 0

Over a field of characteristic zero, a linearly independent family of polynomials has nonzero Hasse Wronskian.

theorem Polynomial.linearIndependent_iff_hasseWronskian_ne_zero {m : ℕ} {K : Type u_3} [Field K] [CharZero K] {g : Fin m → Polynomial K} : LinearIndependent K g ↔ hasseWronskian g ≠ 0

The Wronskian criterion. Over a field of characteristic zero, a family of polynomials is linearly independent if and only if its Hasse Wronskian is nonzero.