Ordinary Wronskians over differential fields

Corvaja--Zannier's positive-characteristic argument uses an ordinary Wronskian over the subfield of constants of a derivation. This file proves the required algebraic criterion: a finite family is linearly independent over the exact constant field if and only if its Wronskian determinant is nonzero.

The reverse implication is the difficult direction. Its proof normalizes a nonzero kernel vector, differentiates the resulting row relations, deletes the normalized coordinate, and applies induction to the smaller Wronskian.

def BGS.Algebra.derivationWronskian {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (D : Derivation C L L) {n : ℕ} (f : Fin n → L) : Matrix (Fin n) (Fin n) L

The ordinary Wronskian matrix of a finite family with respect to a derivation.

Equations

• BGS.Algebra.derivationWronskian D f i j = (↑D ^ ↑i) (f j)

theorem BGS.Algebra.derivationWronskian_det_ne_zero_of_linearIndependent {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (D : Derivation C L L) (constants : ∀ (x : L), D x = 0 → ∃ (c : C), (algebraMap C L) c = x) (n : ℕ) (f : Fin n → L) : LinearIndependent C f → (derivationWronskian D f).det ≠ 0

If every element killed by D comes from C, then a family linearly independent over C has nonzero ordinary Wronskian.

theorem BGS.Algebra.linearIndependent_of_derivationWronskian_det_ne_zero {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (D : Derivation C L L) {n : ℕ} (f : Fin n → L) (hdet : (derivationWronskian D f).det ≠ 0) : LinearIndependent C f

A nonzero Wronskian determinant implies linear independence over the derivation's scalar field.

theorem BGS.Algebra.derivationWronskian_det_ne_zero_iff_linearIndependent {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (D : Derivation C L L) (constants : ∀ (x : L), D x = 0 → ∃ (c : C), (algebraMap C L) c = x) {n : ℕ} (f : Fin n → L) : (derivationWronskian D f).det ≠ 0 ↔ LinearIndependent C f

The ordinary Wronskian criterion when C is exactly the field of constants of D.