search

ImperialCollegeLondon / FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Apache License 2.0
201 stars 39 forks source link

FROBENIUS: descent of char poly from B to A #143

Open kbuzzard opened 20 hours ago

kbuzzard commented 20 hours ago

For the mathematical background, see the blueprint.

We have a ring hom A -> B with image the G-fixed elements, and a polynomial in B[X] which is G-stable descends back to A[X]; furthermore any nice properties (in particular, being monic of degree |G| and having b as as root) also descend.

Right now in the Lean I attempt to do this in quite a bad way, writing down a set-theoretic section from B to A and applying it to the polynomial. @morrison-daniel has suggested a better way here so the argument should be refactored to use his definition of M. This will make things much easier.

kbuzzard commented 14 hours ago

The thorems were proved by Ruben van de Velde without the refactor.