[Merged by Bors] - feat: Mason-Stothers theorem (polynomial ABC)

Mathlib.lean

@@ -3616,6 +3616,7 @@ import Mathlib.NumberTheory.EulerProduct.Basic
 import Mathlib.NumberTheory.EulerProduct.DirichletLSeries
 import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.NumberTheory.FLT.Four
+import Mathlib.NumberTheory.FLT.MasonStothers
 import Mathlib.NumberTheory.FLT.Three
 import Mathlib.NumberTheory.FactorisationProperties
 import Mathlib.NumberTheory.Fermat

Mathlib/NumberTheory/FLT/MasonStothers.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2024 Jineon Baek 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.RingTheory.Polynomial.Radical
+
+/-!
+# Mason-Stothers theorem
+
+This file states and proves Mason-Stothers theorem, which is a polynomial version of ABC conjecture.
+For a (pairwise) coprime polynomials `a, b, c` (over a field) with `a + b + c = 0`, we have
+`max {deg(a), deg(b), deg(c)} + 1 ≤ deg(rad(abc))` or `a' = b' = c' = 0`.
+
+Proof is based on this online note by Franz Lemmermeyer http://www.fen.bilkent.edu.tr/~franz/ag05/ag-02.pdf,
+which is essentially based on Noah Snyder's paper "An Alternative Proof of Mason's Theorem",
+but slightly different.
+
+## TODO
+
+Prove polynomial FLT using Mason-Stothers theorem.
+-/
+
+noncomputable section
+
+open scoped Classical
+
+open Polynomial UniqueFactorizationMonoid UniqueFactorizationDomain EuclideanDomain
+
+variable {k : Type*} [Field k]
+
+private theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian a b) (ha : a ≠ 0)
+    (hb : b ≠ 0) (hc : c ≠ 0) (abc_dr_dvd_w : divRadical (a * b * c) ∣ w) :
+      c.natDegree + 1 ≤ (radical (a * b * c)).natDegree := by
+  have hab := mul_ne_zero ha hb
+  have habc := mul_ne_zero hab hc
+  set abc_dr_nd := (divRadical (a * b * c)).natDegree with def_abc_dr_nd
+  set abc_r_nd := (radical (a * b * c)).natDegree with def_abc_r_nd
+  have t11 : abc_dr_nd < a.natDegree + b.natDegree := by
+    calc
+      abc_dr_nd ≤ w.natDegree := Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw
+      _ < a.natDegree + b.natDegree := by rw [wab] at hw ⊢; exact natDegree_wronskian_lt_add hw
+  have t4 : abc_dr_nd + abc_r_nd < a.natDegree + b.natDegree + abc_r_nd :=
+    Nat.add_lt_add_right t11 abc_r_nd
+  have t3 : abc_dr_nd + abc_r_nd = a.natDegree + b.natDegree + c.natDegree := by
+    calc
+      abc_dr_nd + abc_r_nd = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
+        rw [←
+          Polynomial.natDegree_mul (divRadical_ne_zero habc) (radical_ne_zero (a * b * c))]
+      _ = (a * b * c).natDegree := by
+        rw [mul_comm _ (radical _)]; rw [radical_mul_divRadical (a * b * c)]
+      _ = a.natDegree + b.natDegree + c.natDegree := by
+        rw [Polynomial.natDegree_mul hab hc, Polynomial.natDegree_mul ha hb]
+  rw [t3] at t4
+  exact Nat.lt_of_add_lt_add_left t4
+
+/-- **Polynomial ABC theorem.** -/
+theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
+    (hbc : IsCoprime b c) (hca : IsCoprime c a) (hsum : a + b + c = 0) :
+    (
+      natDegree a + 1 ≤ (radical (a * b * c)).natDegree ∧
+      natDegree b + 1 ≤ (radical (a * b * c)).natDegree ∧
+      natDegree c + 1 ≤ (radical (a * b * c)).natDegree
+    ) ∨
+      derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0 := by
+  -- Utility assertions
+  have wbc := wronskian_eq_of_sum_zero hsum
+  set w := wronskian a b with wab
+  have wca : w = wronskian c a := by
+    rw [add_rotate] at hsum
+    have h := wronskian_eq_of_sum_zero hsum
+    rw [← wbc] at h; exact h
+  have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by
+    have adr_dvd_w := divRadical_dvd_wronskian_left a b
+    have bdr_dvd_w := divRadical_dvd_wronskian_right a b
+    have cdr_dvd_w := divRadical_dvd_wronskian_right b c
+    rw [← wab] at adr_dvd_w bdr_dvd_w
+    rw [← wbc] at cdr_dvd_w
+    have cop_ab_dr := hab.divRadical
+    have cop_bc_dr := hbc.divRadical
+    have cop_ca_dr := hca.divRadical
+    have cop_abc_dr := cop_ca_dr.symm.mul_left cop_bc_dr
+    have abdr_dvd_w := cop_ab_dr.mul_dvd adr_dvd_w bdr_dvd_w
+    have abcdr_dvd_w := cop_abc_dr.mul_dvd abdr_dvd_w cdr_dvd_w
+    convert abcdr_dvd_w using 1
+    rw [← divRadical_mul hab]
+    rw [← divRadical_mul]
+    exact hca.symm.mul_left hbc
+  by_cases hw : w = 0
+  · right
+    rw [hw] at wab wbc
+    cases' hab.wronskian_eq_zero_iff.mp wab.symm with ga gb
+    cases' hbc.wronskian_eq_zero_iff.mp wbc.symm with _ gc
+    exact ⟨ga, gb, gc⟩
+  · left
+    refine ⟨?_, ?_, ?_⟩
+    · rw [mul_rotate] at abc_dr_dvd_w ⊢
+      apply abc_subcall wbc <;> assumption
+    · rw [← mul_rotate] at abc_dr_dvd_w ⊢
+      apply abc_subcall wca <;> assumption
+    · apply abc_subcall wab <;> assumption

Mathlib/RingTheory/Polynomial/Wronskian.lean

@@ -128,7 +128,7 @@ theorem dvd_derivative_iff {a : k[X]} : a ∣ derivative a ↔ derivative a = 0
 For coprime polynomials `a` and `b`, their Wronskian is zero
 if and only if their derivatives are zeros.
 -/
-theorem IsCoprime.wronskian_eq_zero_iff {a b : k[X]} (hc : IsCoprime a b) :
+theorem _root_.IsCoprime.wronskian_eq_zero_iff {a b : k[X]} (hc : IsCoprime a b) :
     wronskian a b = 0 ↔ derivative a = 0 ∧ derivative b = 0 where
   mp hw := by
     rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw