Frobenius constants and ordinary Wronskians

A Frobenius-separating parameter supplies a derivation whose exact constant field is the Frobenius subfield. Combining that construction with the ordinary differential-field Wronskian criterion gives the algebraic Wronskian boundary used in the Corvaja--Zannier argument.

theorem BGS.CorvajaZannier.exists_derivation_with_exact_constants_and_wronskian_criterion {L : Type u_1} [Field L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ∉ frobeniusSubfield L p) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : ∃ (D : Derivation (↥(frobeniusSubfield L p)) L L), D z = 1 ∧ (∀ (x : L), D x = 0 ↔ ∃ (c : ↥(frobeniusSubfield L p)), (algebraMap (↥(frobeniusSubfield L p)) L) c = x) ∧ ∀ (n : ℕ) (f : Fin n → L), (Algebra.derivationWronskian D f).det ≠ 0 ↔ LinearIndependent (↥(frobeniusSubfield L p)) f

A Frobenius-separating parameter gives a derivation normalized by D z = 1, with exact constant field L^p, for which every finite family has nonzero ordinary Wronskian exactly when it is linearly independent over L^p.