Skip to content

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

Closed
seewoo5 wants to merge 37 commits intomasterfrom
feature/mason-stothers
Closed

[Merged by Bors] - feat: Mason-Stothers theorem (polynomial ABC)#15706
seewoo5 wants to merge 37 commits intomasterfrom
feature/mason-stothers

Conversation

@seewoo5
Copy link
Copy Markdown
Collaborator

@seewoo5 seewoo5 commented Aug 11, 2024 •
edited by YaelDillies
Loading

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$.

Almost last part of porting project of the formalization of polynomial ABC.

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

Related: #16060

Open in Gitpod

@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
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 11, 2024 •
edited
Loading

PR summary 8b3a2a85ac

Import changes for modified files

No significant changes to the import graph

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

Declarations diff

+ Polynomial.abc
+ _root_.IsCoprime.wronskian_eq_zero_iff
- IsCoprime.wronskian_eq_zero_iff

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.

@ghost ghost added blocked-by-other-PR This PR depends on another PR (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
jcpaik
jcpaik reviewed Aug 19, 2024
View reviewed changes
@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 (this label is automatically managed by a bot) label Oct 26, 2024
YaelDillies
YaelDillies approved these changes Nov 6, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

maintainer merge

apart from that. Thanks!

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 6, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 6, 2024
@seewoo5 @YaelDillies
Apply suggestions from code review
0d43a0e 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@seewoo5 seewoo5 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 6, 2024
riccardobrasca
riccardobrasca reviewed Nov 7, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

I find the proof easier to read without too many have statement. On the other hand, can you add a little bit of math explanation?

I am not delegating it immediately since I suspect there is a diamond somewhere, let me investigate this.

@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Nov 7, 2024

I pushed a small modification to another file. The lines

noncomputable section

open scoped Classical

can now be removed, adding [DecidableEq k]. I suggest a slightly modified proof of the main result:

/-- **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
    simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
  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
    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

@jcpaik
Copy link
Copy Markdown
Collaborator

jcpaik commented Nov 7, 2024

I am not delegating it immediately since I suspect there is a diamond somewhere, let me investigate this.

I don't get what you mean by this. Are you saying that there is a diamond (I suppose the diamond problem of instance?) in this PR, or some other part of the mathlib that this PR depends on?

jcpaik and others added 3 commits November 7, 2024 20:58
@jcpaik @riccardobrasca
Apply suggestions from code review
c7256cd 
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
@jcpaik
Address comments + tidy up proof
2ffd905
@jcpaik @github-actions
lint
8b3a2a8 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Nov 7, 2024

I am not delegating it immediately since I suspect there is a diamond somewhere, let me investigate this.

I don't get what you mean by this. Are you saying that there is a diamond (I suppose the diamond problem of instance?) in this PR, or some other part of the mathlib that this PR depends on?

It's in another file, but it is fixed by my commit, you can forget about it.

riccardobrasca
riccardobrasca reviewed Nov 7, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 7, 2024

✌️ seewoo5 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 7, 2024
@seewoo5
Copy link
Copy Markdown
Collaborator Author

seewoo5 commented Nov 7, 2024

Thank you all!

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Nov 7, 2024
@seewoo5 @riccardobrasca @jcpaik
feat: Mason-Stothers theorem (polynomial ABC) (#15706)
c5adc80 
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 <riccardo.brasca@gmail.com>
Co-authored-by: Jineon Baek <34874130+jcpaik@users.noreply.github.com>
Co-authored-by: Jineon Baek <jineon@umich.edu>
Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local>
Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 7, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Mason-Stothers theorem (polynomial ABC) [Merged by Bors] - feat: Mason-Stothers theorem (polynomial ABC) Nov 7, 2024
@mathlib-bors mathlib-bors bot closed this Nov 7, 2024
@mathlib-bors mathlib-bors bot deleted the feature/mason-stothers branch November 7, 2024 17:50
@seewoo5 seewoo5 mentioned this pull request Nov 16, 2024
Closed
7 tasks
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@seewoo5 @TobiasLeichtfried
feat: IsCoprime.wronskian_eq_zero_iff (#18483)
38a9b86 
Add `IsCoprime.wronskian_eq_zero_iff`: For two polynomials $a, b \in k[x]$ over a field, $W(a, b) = 0$ if and only if $a' = b' = 0$. This is a part of PR #15706.
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@seewoo5 @riccardobrasca
@jcpaik @TobiasLeichtfried
feat: Mason-Stothers theorem (polynomial ABC) (#15706)
487d366 
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 <riccardo.brasca@gmail.com>
Co-authored-by: Jineon Baek <34874130+jcpaik@users.noreply.github.com>
Co-authored-by: Jineon Baek <jineon@umich.edu>
Co-authored-by: Jineon Baek <jcpaik@jcpaik-desktop.local>
Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
@seewoo5 seewoo5 mentioned this pull request Jan 6, 2025
Closed
5 tasks
mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2025
@seewoo5 @jcpaik
feat: Polynomial FLT (#18882)
ee71c31 
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 <jineon@umich.edu>
Co-authored-by: Jineon Baek <34874130+jcpaik@users.noreply.github.com>
Co-authored-by: Seewoo Lee <seewoo5@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@jcpaik jcpaik jcpaik left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@jcpaik jcpaik

@seewoo5 seewoo5

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@seewoo5 @YaelDillies @mathlib4-dependent-issues-bot @riccardobrasca @jcpaik @grunweg @leanprover-community-bot-assistant