feat: Mason-Stothers theorem (polynomial ABC) (#15706)

This file proves Mason-Stothers theorem (i.e. polynomial ABC). For coprime polynomials $a, b, c$ over a field (of arbitrary characteristic) with $a + b + c = 0$, we have $\max\{\deg(a), \deg(b), \deg(c)\} + 1 \le \deg(\mathrm{rad}(abc))$ or $a' = b' = c' = 0$.



Co-authored-by: Riccardo Brasca <[email protected]>
Co-authored-by: Jineon Baek <[email protected]>
Co-authored-by: Jineon Baek <[email protected]>
Co-authored-by: Jineon Baek <[email protected]>
Co-authored-by: Seewoo Lee <[email protected]>

Author: 4 people

Mathlib.lean

@@ -3617,6 +3617,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,88 @@
+/-
+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 the Mason-Stothers theorem, which is a polynomial version of the
+ABC conjecture. For (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.
+-/
+
+open Polynomial UniqueFactorizationMonoid UniqueFactorizationDomain EuclideanDomain
+
+variable {k : Type*} [Field k] [DecidableEq k]
+
+-- we use this three times; the assumptions are symmetric in a, b, c.
+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 ab_nz := mul_ne_zero ha hb
+  have abc_nz := mul_ne_zero ab_nz hc
+  -- bound the degree of `divRadical (a * b * c)` using Wronskian `w`
+  set abc_dr := divRadical (a * b * c)
+  have abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree := by
+    calc
+      abc_dr.natDegree ≤ 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
+  -- add the degree of `radical (a * b * c)` to both sides and rearrange
+  set abc_r := radical (a * b * c)
+  apply Nat.lt_of_add_lt_add_left
+  calc
+    a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
+      rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
+    _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
+      rw [mul_comm _ (radical _), radical_mul_divRadical (a * b * c)]
+    _ = abc_dr.natDegree + abc_r.natDegree := by
+      rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) (radical_ne_zero (a * b * c))]
+    _ < a.natDegree + b.natDegree + abc_r.natDegree := by
+      exact Nat.add_lt_add_right abc_dr_ndeg_lt _
+
+/-- **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
+  set w := wronskian a b with wab
+  have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
+  have wca : w = wronskian c a := by
+    rw [add_rotate] at hsum
+    simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
+  -- have `divRadical x` dividing `w` for `x = a, b, c`, and use coprimality
+  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
+    rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
+    exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
+      (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w
+  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
+    -- use the subcall three times, using the symmetry in `a, b, c`
+    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/Radical.lean

@@ -14,13 +14,9 @@ This file proves some theorems on `radical` and `divRadical` of polynomials.
 See `RingTheory.Radical` for the definition of `radical` and `divRadical`.
 -/
 
-noncomputable section
-
-open scoped Classical
-
 open Polynomial UniqueFactorizationMonoid UniqueFactorizationDomain EuclideanDomain
 
-variable {k : Type*} [Field k]
+variable {k : Type*} [Field k] [DecidableEq k]
 
 theorem divRadical_dvd_derivative (a : k[X]) : divRadical a ∣ derivative a := by
   induction a using induction_on_coprime

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