search

seewoo5 / lean-poly-abc

Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4
8 stars 0 forks source link

Constant in FLT-Catalan #29

Closed jcpaik closed 1 year ago

jcpaik commented 1 year ago

Make the conclusion of FLT-Catalan stronger, from implying a'=b'=c'=0 to a, b, c being all constants.

Uses infinite descent to do so.

jcpaik commented 1 year ago

@tb65536 It would be much appreciated if you could have a look (though you don't need to). This is a complete mess right now.

seewoo5 commented 1 year ago

Could you briefly sketch the idea? Is it something like replace $a(t)$ with $a_1(t^p)$ and so on?

jcpaik commented 1 year ago

Our initial conclusion was that: for any solution of $a^p + b^q = c^r$, we have $a'=b'=c'=0$. What I do is to further show that $a, b, c$ are constants. This immediately holds when $g = \text{char } k$ is zero. So we can assume that $g$ is a prime. Then a bit of inspection shows that $a' = 0$ if and only if $a(x)$ is actually a polynomial $a_0(x^g)$ of $x^g$: this is reflected in polynomial.expand_concat. So $a(x)^p + b(x)^q = c(x)^r$ gives $a_0(x^g)^p + b_0(x^g)^q = c_0(x^g)^r$. The evaluation morphism $k[x] \rightarrow k[x]$ sending $x$ to $x^g$ is injective actually, so we also get a new solution $(a_0, b_0, c_0)$ so that $a_0(x)^p + b_0(x)^q = c_0(x)^r$ where the degree of $a_0(x)$ is the degree of $a(x)$ divided by $g$. Repeating this indefinitely is impossible unless $a(x)$ has degree 0 to start with. So $a(x)$ has to be a constant.