Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 24 commits into
base: master
Choose a base branch
from

Conversation

seewoo5
Copy link
Collaborator

@seewoo5 seewoo5 commented Aug 11, 2024


Open in Gitpod

Almost last part of porting project of the formalization of polynomial ABC.
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$.

TODO: After #14720 is merged, add polynomial FLT as a corollary. It is already in here.

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 11, 2024
Copy link

github-actions bot commented Aug 11, 2024

PR summary 108762ec7a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.FLT.MasonStothers 1130

Declarations diff

+ IsCoprime.divRadical
+ IsCoprime.wronskian_eq_zero_iff
+ Polynomial.abc
+ divRadical
+ divRadical_dvd_derivative
+ divRadical_dvd_self
+ divRadical_dvd_wronskian_left
+ divRadical_dvd_wronskian_right
+ divRadical_isUnit
+ divRadical_mul
+ divRadical_ne_zero
+ dvd_derivative_iff
+ eq_divRadical
+ le_max₃_left
+ le_max₃_middle
+ le_max₃_right
+ max₃
+ max₃_add_distrib_right
+ max₃_le
+ max₃_lt
+ max₃_mul_distrib_left
+ mul_radical_divRadical

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 11, 2024


/-- Auxiliary theorems for `max₃ a b c = max (max a b) c`. -/
def max₃ (a b c : Nat) : Nat :=
Copy link
Collaborator

@jcpaik jcpaik Aug 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we want this auxiliary function for maximum of three natural numbers in the statement of Mason--Stothers? I wonder how other parts of mathlib represent maximum values of three numbers.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We usually just write max (max a b) c, or a ⊔ b ⊔ c if you prefer infixes. But also you are using it to state max (max a b) c ≤ d, in which situation we much prefer writing a ≤ d ∧ b ≤ d ∧ c ≤ d

@grunweg grunweg changed the title Mason-Stothers theorem (polynomial ABC) feat: Mason-Stothers theorem (polynomial ABC) Aug 22, 2024
@grunweg grunweg added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Aug 23, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 26, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 26, 2024
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Comment on lines 65 to 179
rwa [divRadical, radical_unit_eq_one hu, EuclideanDomain.div_one]

theorem eq_divRadical {a x : k[X]} (h : (radical a) * x = a) : x = divRadical a := by
apply EuclideanDomain.eq_div_of_mul_eq_left (radical_ne_zero a)
rwa [mul_comm]

theorem divRadical_hMul {a b : k[X]} (hc : IsCoprime a b) :
divRadical (a * b) = (divRadical a) * (divRadical b) := by
by_cases ha : a = 0
· rw [ha, MulZeroClass.zero_mul, divRadical, EuclideanDomain.zero_div, MulZeroClass.zero_mul]
by_cases hb : b = 0
· rw [hb, MulZeroClass.mul_zero, divRadical, EuclideanDomain.zero_div, MulZeroClass.mul_zero]
symm; apply eq_divRadical
rw [radical_mul hc]
rw [mul_mul_mul_comm, hMul_radical_divRadical, hMul_radical_divRadical]

theorem divRadical_dvd_self (a : k[X]) : (divRadical a) ∣ a := by
rw [divRadical]
apply EuclideanDomain.div_dvd_of_dvd
exact radical_dvd_self a

/-
Main lemma: `divRadical a` divides `a'`.
Proof uses `induction_on_coprime` of `UniqueFactorizationDomain`.
-/
theorem divRadical_dvd_derivative (a : k[X]) : (divRadical a) ∣ (derivative a) := by
induction a using induction_on_coprime
· case h0 =>
rw [derivative_zero]
apply dvd_zero
· case h1 a ha =>
exact (divRadical_isUnit ha).dvd
· case hpr p i hp =>
cases i
· rw [pow_zero, derivative_one]
apply dvd_zero
· case succ i =>
rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), hMul_radical_divRadical,
radical_pow_of_prime hp i.succ_pos, derivative_pow_succ, ← mul_assoc]
apply dvd_mul_of_dvd_left
rw [mul_comm, mul_assoc]
apply dvd_mul_of_dvd_right
rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]
· -- If it holds for coprime pair a and b, then it also holds for a * b.
case hcp x y hpxy hx hy =>
have hc : IsCoprime x y :=
EuclideanDomain.isCoprime_of_dvd
(fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
fun p hp _ hpx hpy => hp (hpxy hpx hpy)
rw [divRadical_hMul hc, derivative_mul]
exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)

theorem divRadical_dvd_wronskian_left (a b : k[X]) : (divRadical a) ∣ wronskian a b := by
rw [wronskian]
apply dvd_sub
· apply dvd_mul_of_dvd_left
exact divRadical_dvd_self a
· apply dvd_mul_of_dvd_left
exact divRadical_dvd_derivative a

theorem divRadical_dvd_wronskian_right (a b : k[X]) : (divRadical b) ∣ wronskian a b := by
rw [← wronskian_neg_eq, dvd_neg]
exact divRadical_dvd_wronskian_left _ _

@[simp]
theorem dvd_derivative_iff {a : k[X]} : a ∣ derivative a ↔ derivative a = 0 := by
constructor
· intro h
by_cases a_nz : a = 0
· rw [a_nz]; simp only [derivative_zero]
by_contra deriv_nz
have deriv_lt := degree_derivative_lt a_nz
have le_deriv := Polynomial.degree_le_of_dvd h deriv_nz
have lt_self := le_deriv.trans_lt deriv_lt
simp only [lt_self_iff_false] at lt_self
intro h; rw [h]; simp

theorem IsCoprime.wronskian_eq_zero_iff {a b : k[X]} (hc : IsCoprime a b) :
wronskian a b = 0 ↔ derivative a = 0 ∧ derivative b = 0 := by
constructor
· intro hw
rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw
constructor
· rw [← dvd_derivative_iff]
apply hc.dvd_of_dvd_mul_right
rw [← hw]; exact dvd_mul_right _ _
· rw [← dvd_derivative_iff]
apply hc.symm.dvd_of_dvd_mul_left
rw [hw]; exact dvd_mul_left _ _
intro hdab
cases' hdab with hda hdb
rw [wronskian]
rw [hda, hdb]; simp only [MulZeroClass.mul_zero, MulZeroClass.zero_mul, sub_self]


protected theorem IsCoprime.divRadical {a b : k[X]} (h : IsCoprime a b) :
IsCoprime (divRadical a) (divRadical b) := by
rw [← hMul_radical_divRadical a] at h
rw [← hMul_radical_divRadical b] at h
exact h.of_mul_left_right.of_mul_right_right
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could all of this move to a file under Mathlib.RingTheory.Polynomial? Either Mathlib.RingTheory.Polynomial.Wronskian or a new file Mathlib.RingTheory.Polynomial.DivRadical? And can you make that into a separate PR?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll put under Mathlib.RingTheory.Polynomial then (IMO these theorems are to specific so I'm not sure if it worths to make new files for it).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just realized that first half of the theorems & definition of divRadical actually makes sense for EuclideanDomain as well, but not sure if I put these under the "euclidean domain" files. Do you have any suggestions? I think another way is to put divRadical-related theorems, up to divRadical_dvd_self, in Mathlib.RingTheory.Radical with EuclideanDomain version, and put the rest in Mathlib.RingTheory.Polynomial? (Honestly I've never seen any mathematical proofs using $x / \mathrm{rad}(x)$ except for Mason-Stothers...)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think another way is to put divRadical-related theorems, up to divRadical_dvd_self, in Mathlib.RingTheory.Radical with EuclideanDomain version, and put the rest in Mathlib.RingTheory.Polynomial?

That sounds reasonable, yes

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Honestly I've never seen any mathematical proofs using
𝑥
/
𝑟
𝑎
𝑑
(
𝑥
)
except for Mason-Stothers...

You would be surprised how often people have said that their thing had no other application, just before someone else needed it!

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For dvd_derivative_iff and IsCoprime.wronskian_eq_zero_iff, I think these are also seperate things. I'd put the second one under Mathlib.RingTheory.Polynomial.Wronskian, but this depends on the first theorem and I don't know where's the best place to put it - do you have any suggestions? (these two are not included in #18452 for now)

Copy link
Collaborator

@YaelDillies YaelDillies Oct 30, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No sorry, no suggesyion. I would play around with the code myself but I am momentarily incapactitated by apainful wrist

Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
Mathlib/NumberTheory/FLT/MasonStothers.lean Outdated Show resolved Hide resolved
@YaelDillies
Copy link
Collaborator

Sorry, I see the review process is dragging along. We really want this in mathlib!

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2024
apply abc_subcall wbc <;> assumption
constructor
· rw [rot3_mul, rot3_mul] at abc_dr_dvd_w ⊢
· rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
· rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢
· rw [ mul_rotate] at abc_dr_dvd_w ⊢

rw [← divRadical_hMul hab]
rw [← divRadical_hMul _]
rw [← divRadical_mul hab]
rw [← divRadical_mul _]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
rw [← divRadical_mul _]
rw [← divRadical_mul]

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants