Wronskians and linear independence

The Wronskian of a finite family is the determinant whose rows are its successive derivatives. In a differential field, it is nonzero exactly when the family is linearly independent over the constant field of the derivation when the scalars act faithfully. The constant-field hypothesis is explicit: every element killed by the derivation must come from the scalars. No characteristic assumption is needed with this hypothesis.

Scalar changes of generators multiply the Wronskian by the determinant of the coefficient matrix, so an invertible change of basis preserves its nonvanishing. This law holds over commutative rings. A Wronskian that is a non-zero-divisor implies linear independence over any faithfully acting scalar semiring. In an integral domain, nonvanishing suffices; the converse requires an ambient differential field.

This criterion supplies the nonvanishing required to define ramification divisors of linear series by Wronskians. The differential-field argument follows the Wronskian method in D. M. Goldschmidt, Algebraic Functions and Projective Curves, GTM 215, Springer, 2003.

def Derivation.wronskian {k : Type u_1} {F : Type u_2} [CommSemiring k] [CommRing F] [Algebra k F] (D : Derivation k F F) {n : ℕ} (f : Fin n → F) : F

The Wronskian of f: row i consists of its i-th derivatives. The empty family has Wronskian 1.

theorem Derivation.wronskian_def {k : Type u_1} {F : Type u_2} [CommSemiring k] [CommRing F] [Algebra k F] (D : Derivation k F F) {n : ℕ} (f : Fin n → F) : D.wronskian f = (Matrix.of fun (i j : Fin n) => (⇑D)^[↑i] (f j)).det

The determinant characterizing the Wronskian.

@[simp]

theorem Derivation.wronskian_empty {k : Type u_1} {F : Type u_2} [CommSemiring k] [CommRing F] [Algebra k F] (D : Derivation k F F) (f : Fin 0 → F) : D.wronskian f = 1

@[simp]

theorem Derivation.wronskian_singleton {k : Type u_1} {F : Type u_2} [CommSemiring k] [CommRing F] [Algebra k F] (D : Derivation k F F) (f : Fin 1 → F) : D.wronskian f = f 0

theorem Derivation.wronskian_sum_smul {k : Type u_1} {F : Type u_2} [CommRing k] [CommRing F] [Algebra k F] (D : Derivation k F F) {n : ℕ} (f : Fin n → F) (A : Matrix (Fin n) (Fin n) k) : (D.wronskian fun (j : Fin n) => ∑ i : Fin n, A i j • f i) = D.wronskian f * (algebraMap k F) A.det

A scalar change of generators multiplies the Wronskian by the determinant of its coefficient matrix. The columns of A give the coefficients of the new family.

theorem Derivation.wronskian_sum_smul_ne_zero_iff {k : Type u_1} {F : Type u_2} [CommRing k] [CommRing F] [Algebra k F] (D : Derivation k F F) {n : ℕ} (f : Fin n → F) (A : Matrix (Fin n) (Fin n) k) (hA : IsUnit A.det) : (D.wronskian fun (j : Fin n) => ∑ i : Fin n, A i j • f i) ≠ 0 ↔ D.wronskian f ≠ 0

An invertible scalar change of generators preserves nonvanishing of the Wronskian. This does not require the scalars to contain every constant of the derivation.

theorem Derivation.linearIndependent_of_wronskian_mem_nonZeroDivisors {k : Type u_1} {F : Type u_2} [CommSemiring k] [CommRing F] [Algebra k F] [FaithfulSMul k F] (D : Derivation k F F) {n : ℕ} {f : Fin n → F} (hw : D.wronskian f ∈ nonZeroDivisors F) : LinearIndependent k f

A Wronskian that is a non-zero-divisor implies linear independence over any faithfully acting scalar semiring, even if the derivation has additional constants.

theorem Derivation.linearIndependent_of_wronskian_ne_zero {k : Type u_1} {F : Type u_2} [CommSemiring k] [CommRing F] [NoZeroDivisors F] [Algebra k F] [FaithfulSMul k F] (D : Derivation k F F) {n : ℕ} {f : Fin n → F} (hw : D.wronskian f ≠ 0) : LinearIndependent k f

Nonzero Wronskian implies linear independence over any faithfully acting scalar semiring, even if the derivation has additional constants.

theorem Derivation.wronskian_ne_zero_of_linearIndependent {k : Type u_1} {F : Type u_2} [CommSemiring k] [Field F] [Algebra k F] (D : Derivation k F F) (hconst : ∀ (y : F), D y = 0 → ∃ (a : k), (algebraMap k F) a = y) {n : ℕ} {f : Fin n → F} (hf : LinearIndependent k f) : D.wronskian f ≠ 0

A linearly independent family has nonzero Wronskian if every constant of the derivation comes from the scalars.

theorem Derivation.wronskian_ne_zero_iff {k : Type u_1} {F : Type u_2} [CommSemiring k] [Field F] [Algebra k F] [FaithfulSMul k F] (D : Derivation k F F) (hconst : ∀ (y : F), D y = 0 → ∃ (a : k), (algebraMap k F) a = y) {n : ℕ} (f : Fin n → F) : D.wronskian f ≠ 0 ↔ LinearIndependent k f

The Wronskian detects linear independence when the scalars embed faithfully and contain every constant of the derivation.