Skip to content

Commit ee71c31

Browse files
seewoo5jcpaik
seewoo5
and
jcpaik
committed
feat: Polynomial FLT (#18882)
Prove the polynomial FLT, using Mason-Stothers theorem #15706. More generally, prove non-solvability of Fermat-Catalan equation: $ux^p + vx^q + wz^r = 0$ where $u, v, w \in k^\times$ are units and $p, q, r \ge 3$ with $pq + qr + rp \le pqr$. Also derive the `IsCoprime b c` and `IsCoprime c a` assumptions from the `IsCoprime a b` and `a + b + c = 0` ones in `Polynomial.abc`. Co-authored-by: Jineon Baek <[email protected]> Co-authored-by: Jineon Baek <[email protected]> Co-authored-by: Seewoo Lee <[email protected]>
1 parent 648ca59 commit ee71c31

File tree

3 files changed

+290
-5
lines changed

3 files changed

+290
-5
lines changed

‎Mathlib.lean

+1
Original file line numberDiff line numberDiff line change
@@ -3894,6 +3894,7 @@ import Mathlib.NumberTheory.EulerProduct.ExpLog
38943894
import Mathlib.NumberTheory.FLT.Basic
38953895
import Mathlib.NumberTheory.FLT.Four
38963896
import Mathlib.NumberTheory.FLT.MasonStothers
3897+
import Mathlib.NumberTheory.FLT.Polynomial
38973898
import Mathlib.NumberTheory.FLT.Three
38983899
import Mathlib.NumberTheory.FactorisationProperties
38993900
import Mathlib.NumberTheory.Fermat

‎Mathlib/NumberTheory/FLT/MasonStothers.lean

+14-5
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,6 @@ Proof is based on this online note by Franz Lemmermeyer http://www.fen.bilkent.e
1616
which is essentially based on Noah Snyder's paper "An Alternative Proof of Mason's Theorem",
1717
but slightly different.
1818
19-
## TODO
20-
21-
Prove polynomial FLT using Mason-Stothers theorem.
2219
-/
2320

2421
open Polynomial UniqueFactorizationMonoid UniqueFactorizationDomain EuclideanDomain
@@ -51,13 +48,25 @@ private theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian
5148
exact Nat.add_lt_add_right abc_dr_ndeg_lt _
5249

5350
/-- **Polynomial ABC theorem.** -/
54-
theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
55-
(hbc : IsCoprime b c) (hca : IsCoprime c a) (hsum : a + b + c = 0) :
51+
protected theorem Polynomial.abc
52+
{a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
53+
(hab : IsCoprime a b) (hsum : a + b + c = 0) :
5654
( natDegree a + 1 ≤ (radical (a * b * c)).natDegree ∧
5755
natDegree b + 1 ≤ (radical (a * b * c)).natDegree ∧
5856
natDegree c + 1 ≤ (radical (a * b * c)).natDegree ) ∨
5957
derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0 := by
6058
set w := wronskian a b with wab
59+
have hbc : IsCoprime b c := by
60+
rw [add_eq_zero_iff_neg_eq] at hsum
61+
rw [← hsum, IsCoprime.neg_right_iff]
62+
convert IsCoprime.add_mul_left_right hab.symm 1
63+
rw [mul_one]
64+
have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum
65+
have hca : IsCoprime c a := by
66+
rw [add_eq_zero_iff_neg_eq] at hsum'
67+
rw [← hsum', IsCoprime.neg_right_iff]
68+
convert IsCoprime.add_mul_left_right hbc.symm 1
69+
rw [mul_one]
6170
have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
6271
have wca : w = wronskian c a := by
6372
rw [add_rotate] at hsum

‎Mathlib/NumberTheory/FLT/Polynomial.lean

+275
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,275 @@
1+
/-
2+
Copyright (c) 2024 Jineon Baek and Seewoo Lee. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jineon Baek, Seewoo Lee
5+
-/
6+
import Mathlib.Algebra.Polynomial.Expand
7+
import Mathlib.Algebra.GroupWithZero.Defs
8+
import Mathlib.NumberTheory.FLT.Basic
9+
import Mathlib.NumberTheory.FLT.MasonStothers
10+
import Mathlib.RingTheory.Polynomial.Content
11+
12+
/-!
13+
# Fermat's Last Theorem for polynomials over a field
14+
15+
This file states and proves the Fermat's Last Theorem for polynomials over a field.
16+
For `n ≥ 3` not divisible by the characteristic of the coefficient field `k` and (pairwise) nonzero
17+
coprime polynomials `a, b, c` (over a field) with `a ^ n + b ^ n = c ^ n`,
18+
all polynomials must be constants.
19+
20+
More generally, we can prove non-solvability of the Fermat-Catalan equation: there are no
21+
non-constant polynomial solutions to the equation `u * a ^ p + v * b ^ q + w * c ^ r = 0`, where
22+
`p, q, r ≥ 3` with `p * q + q * r + r * p ≤ p * q * r` , `p, q, r` not divisible by `char k`,
23+
and `u, v, w` are nonzero elements in `k`.
24+
FLT is the special case where `p = q = r = n`, `u = v = 1`, and `w = -1`.
25+
26+
The proof uses the Mason-Stothers theorem (Polynomial ABC theorem) and infinite descent
27+
(in the characteristic p case).
28+
-/
29+
30+
open Polynomial UniqueFactorizationMonoid UniqueFactorizationDomain
31+
32+
variable {k R : Type*} [Field k] [CommRing R] [IsDomain R] [NormalizationMonoid R]
33+
[UniqueFactorizationMonoid R]
34+
35+
private lemma Ne.isUnit_C {u : k} (hu : u ≠ 0) : IsUnit (C u) :=
36+
Polynomial.isUnit_C.mpr hu.isUnit
37+
38+
-- auxiliary lemma that 'rotates' coprimality
39+
private lemma rot_coprime
40+
{p q r : ℕ} {a b c : k[X]} {u v w : k}
41+
{hp : 0 < p} {hq : 0 < q} {hr : 0 < r}
42+
{hu : u ≠ 0} {hv : v ≠ 0} {hw : w ≠ 0}
43+
(heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0) (hab : IsCoprime a b) : IsCoprime b c := by
44+
have hCu : IsUnit (C u) := Ne.isUnit_C hu
45+
have hCv : IsUnit (C v) := Ne.isUnit_C hv
46+
have hCw : IsUnit (C w) := Ne.isUnit_C hw
47+
rw [← IsCoprime.pow_iff hp hq, ← isCoprime_mul_units_left hCu hCv] at hab
48+
rw [add_eq_zero_iff_neg_eq] at heq
49+
rw [← IsCoprime.pow_iff hq hr, ← isCoprime_mul_units_left hCv hCw,
50+
← heq, IsCoprime.neg_right_iff]
51+
convert IsCoprime.add_mul_left_right hab.symm 1 using 2
52+
rw [mul_one]
53+
54+
private lemma ineq_pqr_contradiction {p q r a b c : ℕ}
55+
(hp : 0 < p) (hq : 0 < q) (hr : 0 < r)
56+
(hineq : q * r + r * p + p * q ≤ p * q * r)
57+
(hpa : p * a < a + b + c)
58+
(hqb : q * b < a + b + c)
59+
(hrc : r * c < a + b + c) : False := by
60+
suffices h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c) by simp at h
61+
calc
62+
_ = (p * a) * (q * r) + (q * b) * (r * p) + (r * c) * (p * q) + 1 := by ring
63+
_ ≤ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) := by
64+
rw [Nat.succ_le]
65+
gcongr
66+
_ = (q * r + r * p + p * q) * (a + b + c) := by ring
67+
_ ≤ _ := by gcongr
68+
69+
private theorem Polynomial.flt_catalan_deriv [DecidableEq k]
70+
{p q r : ℕ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r)
71+
(hineq : q * r + r * p + p * q ≤ p * q * r)
72+
(chp : (p : k) ≠ 0) (chq : (q : k) ≠ 0) (chr : (r : k) ≠ 0)
73+
{a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
74+
(hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0)
75+
(heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0) :
76+
derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0 := by
77+
have hbc : IsCoprime b c := by apply rot_coprime heq <;> assumption
78+
have hca : IsCoprime c a := by
79+
rw [add_rotate] at heq; apply rot_coprime heq <;> assumption
80+
have hCu := C_ne_zero.mpr hu
81+
have hCv := C_ne_zero.mpr hv
82+
have hCw := C_ne_zero.mpr hw
83+
have hap := pow_ne_zero p ha
84+
have hbq := pow_ne_zero q hb
85+
have hcr := pow_ne_zero r hc
86+
have habp : IsCoprime (C u * a ^ p) (C v * b ^ q) := by
87+
rw [isCoprime_mul_units_left hu.isUnit_C hv.isUnit_C]; exact hab.pow
88+
have hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r) := by
89+
rw [isCoprime_mul_units_left hv.isUnit_C hw.isUnit_C]; exact hbc.pow
90+
have hcap : IsCoprime (C w * c ^ r) (C u * a ^ p) := by
91+
rw [isCoprime_mul_units_left hw.isUnit_C hu.isUnit_C]; exact hca.pow
92+
have habcp := hcap.symm.mul_left hbcp
93+
94+
-- Use Mason-Stothers theorem
95+
rcases Polynomial.abc
96+
(mul_ne_zero hCu hap) (mul_ne_zero hCv hbq) (mul_ne_zero hCw hcr)
97+
habp heq with nd_lt | dr0
98+
· simp_rw [radical_mul habcp, radical_mul habp,
99+
radical_mul_of_isUnit_left hu.isUnit_C,
100+
radical_mul_of_isUnit_left hv.isUnit_C,
101+
radical_mul_of_isUnit_left hw.isUnit_C,
102+
radical_pow a hp, radical_pow b hq, radical_pow c hr,
103+
natDegree_mul hCu hap,
104+
natDegree_mul hCv hbq,
105+
natDegree_mul hCw hcr,
106+
natDegree_C, natDegree_pow, zero_add,
107+
← radical_mul hab,
108+
← radical_mul (hca.symm.mul_left hbc)] at nd_lt
109+
110+
obtain ⟨hpa', hqb', hrc'⟩ := nd_lt
111+
have hpa := hpa'.trans natDegree_radical_le
112+
have hqb := hqb'.trans natDegree_radical_le
113+
have hrc := hrc'.trans natDegree_radical_le
114+
rw [natDegree_mul (mul_ne_zero ha hb) hc,
115+
natDegree_mul ha hb, Nat.add_one_le_iff] at hpa hqb hrc
116+
exfalso
117+
exact (ineq_pqr_contradiction hp hq hr hineq hpa hqb hrc)
118+
· rw [derivative_C_mul, derivative_C_mul, derivative_C_mul,
119+
mul_eq_zero_iff_left (C_ne_zero.mpr hu),
120+
mul_eq_zero_iff_left (C_ne_zero.mpr hv),
121+
mul_eq_zero_iff_left (C_ne_zero.mpr hw),
122+
derivative_pow_eq_zero chp,
123+
derivative_pow_eq_zero chq,
124+
derivative_pow_eq_zero chr] at dr0
125+
exact dr0
126+
127+
-- helper lemma that gives a baggage of small facts on `contract (ringChar k) a`
128+
private lemma find_contract {a : k[X]}
129+
(ha : a ≠ 0) (hda : derivative a = 0) (chn0 : ringChar k ≠ 0) :
130+
∃ ca, ca ≠ 0 ∧
131+
a = expand k (ringChar k) ca ∧
132+
a.natDegree = ca.natDegree * ringChar k := by
133+
have heq := (expand_contract (ringChar k) hda chn0).symm
134+
refine ⟨contract (ringChar k) a, ?_, heq, ?_⟩
135+
· intro h
136+
rw [h, map_zero] at heq
137+
exact ha heq
138+
· rw [← natDegree_expand, ← heq]
139+
140+
variable [DecidableEq k]
141+
142+
private theorem Polynomial.flt_catalan_aux
143+
{p q r : ℕ} {a b c : k[X]} {u v w : k}
144+
(heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0)
145+
(hp : 0 < p) (hq : 0 < q) (hr : 0 < r)
146+
(hineq : q * r + r * p + p * q ≤ p * q * r)
147+
(chp : (p : k) ≠ 0) (chq : (q : k) ≠ 0) (chr : (r : k) ≠ 0)
148+
(ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
149+
(hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) :
150+
a.natDegree = 0 := by
151+
cases' eq_or_ne (ringChar k) 0 with ch0 chn0
152+
-- characteristic zero
153+
· obtain ⟨da, -, -⟩ := flt_catalan_deriv
154+
hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
155+
have czk : CharZero k := by
156+
apply charZero_of_inj_zero
157+
intro n
158+
rw [ringChar.spec, ch0]
159+
exact zero_dvd_iff.mp
160+
rw [eq_C_of_derivative_eq_zero da]
161+
exact natDegree_C _
162+
-- characteristic p > 0
163+
· generalize eq_d : a.natDegree = d
164+
-- set up infinite descent
165+
-- strong induct on `d := a.natDegree`
166+
induction d
167+
using Nat.case_strong_induction_on
168+
generalizing a b c ha hb hc hab heq with
169+
| hz => rfl
170+
| hi d ih_d => -- have derivatives of `a, b, c` zero
171+
obtain ⟨ad, bd, cd⟩ := flt_catalan_deriv
172+
hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
173+
-- find contracts `ca, cb, cc` so that `a(k) = ca(k^ch)`
174+
obtain ⟨ca, ca_nz, eq_a, eq_deg_a⟩ := find_contract ha ad chn0
175+
obtain ⟨cb, cb_nz, eq_b, eq_deg_b⟩ := find_contract hb bd chn0
176+
obtain ⟨cc, cc_nz, eq_c, eq_deg_c⟩ := find_contract hc cd chn0
177+
set ch := ringChar k
178+
suffices hca : ca.natDegree = 0 by
179+
rw [← eq_d, eq_deg_a, hca, zero_mul]
180+
by_contra hnca; apply hnca
181+
apply ih_d _ _ _ ca_nz cb_nz cc_nz <;> clear ih_d <;> try rfl
182+
· apply (isCoprime_expand chn0).mp
183+
rwa [← eq_a, ← eq_b]
184+
· have _ : ch ≠ 1 := CharP.ringChar_ne_one
185+
have hch2 : 2 ≤ ch := by omega
186+
rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
187+
refine le_trans ?_ (Nat.mul_le_mul_left _ hch2)
188+
omega
189+
· rw [eq_a, eq_b, eq_c, ← expand_C ch u, ← expand_C ch v, ← expand_C ch w] at heq
190+
simp_rw [← map_pow, ← map_mul, ← map_add] at heq
191+
rwa [Polynomial.expand_eq_zero (zero_lt_iff.mpr chn0)] at heq
192+
193+
/-- Nonsolvability of the Fermat-Catalan equation. -/
194+
theorem Polynomial.flt_catalan
195+
{p q r : ℕ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r)
196+
(hineq : q * r + r * p + p * q ≤ p * q * r)
197+
(chp : (p : k) ≠ 0) (chq : (q : k) ≠ 0) (chr : (r : k) ≠ 0)
198+
{a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
199+
{u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0)
200+
(heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0) :
201+
a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0 := by
202+
-- WLOG argument: essentially three times flt_catalan_aux
203+
have hbc : IsCoprime b c := by
204+
apply rot_coprime heq hab <;> assumption
205+
have heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0 := by
206+
rwa [add_rotate] at heq
207+
have hca : IsCoprime c a := by
208+
apply rot_coprime heq' hbc <;> assumption
209+
refine ⟨?_, ?_, ?_⟩
210+
· apply flt_catalan_aux heq <;> assumption
211+
· rw [add_rotate] at heq hineq
212+
rw [mul_rotate] at hineq
213+
apply flt_catalan_aux heq <;> assumption
214+
· rw [← add_rotate] at heq hineq
215+
rw [← mul_rotate] at hineq
216+
apply flt_catalan_aux heq <;> assumption
217+
218+
theorem Polynomial.flt
219+
{n : ℕ} (hn : 3 ≤ n) (chn : (n : k) ≠ 0)
220+
{a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
221+
(hab : IsCoprime a b) (heq : a ^ n + b ^ n = c ^ n) :
222+
a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0 := by
223+
have hn' : 0 < n := by linarith
224+
rw [← sub_eq_zero, ← one_mul (a ^ n), ← one_mul (b ^ n), ← one_mul (c ^ n), sub_eq_add_neg,
225+
← neg_mul] at heq
226+
have hone : (1 : k[X]) = C 1 := by rfl
227+
have hneg_one : (-1 : k[X]) = C (-1) := by simp only [map_neg, map_one]
228+
simp_rw [hneg_one, hone] at heq
229+
apply flt_catalan hn' hn' hn' _
230+
chn chn chn ha hb hc hab one_ne_zero one_ne_zero (neg_ne_zero.mpr one_ne_zero) heq
231+
have eq_lhs : n * n + n * n + n * n = 3 * n * n := by ring
232+
rw [eq_lhs, mul_assoc, mul_assoc]
233+
exact Nat.mul_le_mul_right (n * n) hn
234+
235+
theorem fermatLastTheoremWith'_polynomial {n : ℕ} (hn : 3 ≤ n) (chn : (n : k) ≠ 0) :
236+
FermatLastTheoremWith' k[X] n := by
237+
rw [FermatLastTheoremWith']
238+
intros a b c ha hb hc heq
239+
obtain ⟨a', eq_a⟩ := gcd_dvd_left a b
240+
obtain ⟨b', eq_b⟩ := gcd_dvd_right a b
241+
set d := gcd a b
242+
have hd : d ≠ 0 := gcd_ne_zero_of_left ha
243+
rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
244+
have hdc : d ∣ c := by
245+
have hn : 0 < n := by omega
246+
have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
247+
248+
rw [dvd_iff_normalizedFactors_le_normalizedFactors hd hc]
249+
rw [dvd_iff_normalizedFactors_le_normalizedFactors
250+
(pow_ne_zero n hd) (pow_ne_zero n hc),
251+
normalizedFactors_pow, normalizedFactors_pow] at hdncn
252+
simp_rw [Multiset.le_iff_count, Multiset.count_nsmul,
253+
mul_le_mul_left hn] at hdncn ⊢
254+
exact hdncn
255+
obtain ⟨c', eq_c⟩ := hdc
256+
rw [eq_a, mul_ne_zero_iff] at ha
257+
rw [eq_b, mul_ne_zero_iff] at hb
258+
rw [eq_c, mul_ne_zero_iff] at hc
259+
rw [mul_comm] at eq_a eq_b eq_c
260+
refine ⟨d, a', b', c', ⟨eq_a, eq_b, eq_c⟩, ?_⟩
261+
rw [eq_c, mul_pow, mul_comm, mul_left_inj' (pow_ne_zero n hd)] at heq
262+
suffices goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0 by
263+
simp [natDegree_eq_zero] at goal
264+
obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
265+
rw [← ha', ← hb', ← hc']
266+
rw [← ha', C_ne_zero] at ha
267+
rw [← hb', C_ne_zero] at hb
268+
rw [← hc', C_ne_zero] at hc
269+
exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
270+
apply flt hn chn ha.right hb.right hc.right _ heq
271+
convert isCoprime_div_gcd_div_gcd _
272+
· exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm
273+
· exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm
274+
· rw [eq_b]
275+
exact mul_ne_zero hb.right hb.left

0 commit comments

Comments
 (0)