feat: add polynomial Wronskian (#14243)

Define wronskian for polynomials over commutative rings, and prove some basic properties. This is mainly for the porting of our (me and @jcpaik) formalization of [Mason-Stothers theorem](https://github.com/seewoo5/lean-poly-abc). We already discussed about this in [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Ring.20with.20derivation/near/447378869). Especially, it may possible to improve as
* Replace `CommRing` with `Ring`
* or more generally, Wronskian can be defined over any ring with `Derivation`, and most of the theorems we proved should also hold in this context



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Seewoo Lee <[email protected]>

Mathlib.lean

@@ -3775,6 +3775,7 @@ import Mathlib.RingTheory.Polynomial.Selmer
 import Mathlib.RingTheory.Polynomial.SeparableDegree
 import Mathlib.RingTheory.Polynomial.Tower
 import Mathlib.RingTheory.Polynomial.Vieta
+import Mathlib.RingTheory.Polynomial.Wronskian
 import Mathlib.RingTheory.PolynomialAlgebra
 import Mathlib.RingTheory.PowerBasis
 import Mathlib.RingTheory.PowerSeries.Basic

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

@@ -119,6 +119,8 @@ theorem degree_eq_bot : degree p = ⊥ ↔ p = 0 :=
   ⟨fun h => support_eq_empty.1 (Finset.max_eq_bot.1 h), fun h => h.symm ▸ rfl⟩
 #align polynomial.degree_eq_bot Polynomial.degree_eq_bot
 
+theorem degree_ne_bot : degree p ≠ ⊥ ↔ p ≠ 0 := degree_eq_bot.not
+
 @[nontriviality]
 theorem degree_of_subsingleton [Subsingleton R] : degree p = ⊥ := by
   rw [Subsingleton.elim p 0, degree_zero]

Mathlib/RingTheory/Polynomial/Wronskian.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2024 Jineon Back and Seewoo Lee. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jineon Baek, Seewoo Lee
+-/
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.Algebra.Polynomial.Derivative
+import Mathlib.LinearAlgebra.SesquilinearForm
+
+/-!
+# Wronskian of a pair of polynomial
+
+This file defines Wronskian of a pair of polynomials, which is `W(a, b) = ab' - a'b`.
+We also prove basic properties of it.
+
+## Main declarations
+
+- `Polynomial.wronskian_eq_of_sum_zero`: We have `W(a, b) = W(b, c)` when `a + b + c = 0`.
+- `Polynomial.degree_wronskian_lt_add`: Degree of Wronskian `W(a, b)` is strictly smaller than
+  the sum of degrees of `a` and `b`
+- `Polynomial.natDegree_wronskian_lt_add`: `natDegree` version of the above theorem.
+  We need to assume that the Wronskian is nonzero. (Otherwise, `a = b = 1` gives a counterexample.)
+
+## TODO
+
+- Define Wronskian for n-tuple of polynomials, not necessarily two.
+-/
+
+noncomputable section
+
+open scoped Polynomial
+
+namespace Polynomial
+
+variable {R : Type*} [CommRing R]
+
+/-- Wronskian of a pair of polynomials, `W(a, b) = ab' - a'b`. -/
+def wronskian (a b : R[X]) : R[X] :=
+  a * (derivative b) - (derivative a) * b
+
+variable (R) in
+/-- `Polynomial.wronskian` as a bilinear map. -/
+def wronskianBilin : R[X] →ₗ[R] R[X] →ₗ[R] R[X] :=
+  (LinearMap.mul R R[X]).compl₂ derivative - (LinearMap.mul R R[X]).comp derivative
+
+@[simp]
+theorem wronskianBilin_apply (a b : R[X]) : wronskianBilin R a b = wronskian a b := rfl
+
+@[simp]
+theorem wronskian_zero_left (a : R[X]) : wronskian 0 a = 0 := by
+  rw [← wronskianBilin_apply 0 a, map_zero]; rfl
+
+@[simp]
+theorem wronskian_zero_right (a : R[X]) : wronskian a 0 = 0 := (wronskianBilin R a).map_zero
+
+theorem wronskian_neg_left (a b : R[X]) : wronskian (-a) b = -wronskian a b :=
+  LinearMap.map_neg₂ (wronskianBilin R) a b
+
+theorem wronskian_neg_right (a b : R[X]) : wronskian a (-b) = -wronskian a b :=
+  (wronskianBilin R a).map_neg b
+
+theorem wronskian_add_right (a b c : R[X]) : wronskian a (b + c) = wronskian a b + wronskian a c :=
+  (wronskianBilin R a).map_add b c
+
+theorem wronskian_add_left (a b c : R[X]) : wronskian (a + b) c = wronskian a c + wronskian b c :=
+  (wronskianBilin R).map_add₂ a b c
+
+theorem wronskian_self_eq_zero (a : R[X]) : wronskian a a = 0 := by
+  rw [wronskian, mul_comm, sub_self]
+
+theorem isAlt_wronskianBilin : (wronskianBilin R).IsAlt := wronskian_self_eq_zero
+
+theorem wronskian_neg_eq (a b : R[X]) : -wronskian a b = wronskian b a :=
+  LinearMap.IsAlt.neg isAlt_wronskianBilin a b
+
+theorem wronskian_eq_of_sum_zero {a b c : R[X]} (hAdd : a + b + c = 0) :
+    wronskian a b = wronskian b c := isAlt_wronskianBilin.eq_of_add_add_eq_zero hAdd
+
+/-- Degree of `W(a,b)` is strictly less than the sum of degrees of `a` and `b` (both nonzero). -/
+theorem degree_wronskian_lt_add {a b : R[X]} (ha : a ≠ 0) (hb : b ≠ 0) :
+    (wronskian a b).degree < a.degree + b.degree := by
+  calc
+    (wronskian a b).degree ≤ max (a * derivative b).degree (derivative a * b).degree :=
+      Polynomial.degree_sub_le _ _
+    _ < a.degree + b.degree := by
+      rw [max_lt_iff]
+      constructor
+      case left =>
+        apply lt_of_le_of_lt
+        exact degree_mul_le a (derivative b)
+        rw [← Polynomial.degree_ne_bot] at ha
+        rw [WithBot.add_lt_add_iff_left ha]
+        exact Polynomial.degree_derivative_lt hb
+      case right =>
+        apply lt_of_le_of_lt
+        exact degree_mul_le (derivative a) b
+        rw [← Polynomial.degree_ne_bot] at hb
+        rw [WithBot.add_lt_add_iff_right hb]
+        exact Polynomial.degree_derivative_lt ha
+
+/--
+`natDegree` version of the above theorem.
+Note this would be false with just `(ha : a ≠ 0) (hb : b ≠ 0),
+as when `a = b = 1` we have `(wronskian a b).natDegree = a.natDegree = b.natDegree = 0`.
+-/
+theorem natDegree_wronskian_lt_add {a b : R[X]} (hw : wronskian a b ≠ 0) :
+    (wronskian a b).natDegree < a.natDegree + b.natDegree := by
+  have ha : a ≠ 0 := by intro h; subst h; rw [wronskian_zero_left] at hw; exact hw rfl
+  have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl
+  rw [← WithBot.coe_lt_coe, WithBot.coe_add]
+  convert ← degree_wronskian_lt_add ha hb
+  · exact Polynomial.degree_eq_natDegree hw
+  · exact Polynomial.degree_eq_natDegree ha
+  · exact Polynomial.degree_eq_natDegree hb