Notes on the proof of FLT which is being formalized

Stream: FLT

[Kevin Buzzard]

People have asked me "which proof of FLT exactly are you formalizing?" and my answer has always been the not particularly adequate "Richard Taylor and I had a big discussion about this last year and there is a secret 14 page document which I have not made public but I will very slowly be blueprintizing it".

I now have a much much better answer. Taylor has been giving a graduate course in Stanford about the approach, and his student Daniel Kim has been taking notes and putting them online; they are here.

Daniel has asked me to stress that everything here is unrefereed (and the course is still running) and if anyone finds any inaccuracies or anything unclear then they should perhaps raise the issue on this thread and I can feed back to Daniel.

For those just looking for a summary: key differences between our approach and the original Taylor-Wiles approach are:

(1) we argue at p rather than at 3 to prove the Frey curve doesn't exist, hence we don't need Langlands--Tunnell, but we do need Mazur to check that the p-torsion is irreducible.

(2) we use the Skinner-Wiles trick to do level-lowering (making global solvable extensions to kill local ramification) so we need cyclic base change and we need all the R=T theorems to work for Hilbert modular forms; however we don't need Ribet's level-lowering theorem.

(3) By "cyclic base change" I mean that we need it for GL_2/(totally real field) but all the Hecke algebras will be defined for totally definite quaternion algebras, and we need multiplicity 1 theorems for them too in order to classify the image of base change; these mult 1 theorems will be proved using Jacquet-Langlands and mult 1 for GL_2, all of which I will be assuming for now.

(4) Likewise I will be assuming the existence of Galois reps associated to Hilbert modular forms for now (we need it in the disc(D)=1 case so we'll have to switch to a unitary Shimura surface and compute its H^2).

(5) We don't need an R=T theorem, we only need a modularity lifting theorem so "R=T up to torsion". Andrew Yang has already formalized the minimal level version of this.

(6) One thing we need but Wiles didn't need is the following theorem: if $K/\mathbb{Q}$ is a finite Galois extension with discriminant $D$, and if $D^{1/[K:\mathbb{Q}]}<8.25$ then $[K:\mathbb{Q}]<18$. The only reference I know for this is the tables of Diaz y Diaz (F. Diaz y Diaz, Tables minorant la racine n-ième du discriminant d’un corps de degré n,
Publ. Math. d’Orsay, 1980) but IIRC there is no proof there?

[Notification Bot]

14 messages were moved from this topic to #FLT > Odlyzko bounds by Kevin Buzzard.