4 An overview of the proof

So far we have seen that, modulo Mazur’s theorem (and various other things which will still take some work to formalise but which are much easier), Fermat’s Last Theorem can be reduced to the statement that there is no prime \(\ell \geq 5\) and hardly-ramified irreducible 2-dimensional Galois representation \(\rho :\operatorname{Gal}(\overline{\mathbb {Q}}/\mathbb {Q})\to \operatorname{GL}_2(\mathbb {Z}/\ell \mathbb {Z})\).

In this chapter we give an overview of our strategy for proving this, and collect various results which we will need along the way. Note that we no longer need to assume that \(\rho \) comes from the \(\ell \)-torsion in an elliptic curve.

4.1 Potential modularity.

We will only speak about modularity for 2-dimensional representations of the absolute Galois group of a totally real field \(F\) of even degree over \(\mathbb {Q}\), and in particular we will never say that a representation of the absolute Galois group of \(\mathbb {Q}\) is modular! What we will mean by “modular” is “associated to an automorphic representation of the units of the totally definite quaternion algebra over \(F\) ramified at no finite places”. We can furthermore even demand that the infinity type is trivial, as these are the only forms we shall need for FLT.

Assume we have a hardly-ramified representation \(\rho \) as above. Let \(K\) be the number field corresponding to the kernel of \(\rho \). Our first claim is that there is some totally real field \(F\) of even degree, Galois over \(\mathbb {Q}\), unramified at \(\ell \), and disjoint from \(K\), such that \(\rho |G_F\) is modular. The proof of this is very long, and uses a host of machinery. For example:

• Moret–Bailly’s result  [ 10 ] on points on curves with prescribed local behaviour;

• several nontrivial results in global class field theory;

• the Jacquet–Langlands correspondence;

• The assertion that irreducible 2-dimensional mod \(p\) representations induced from a character are modular (this follows from converse theorems);

• A modularity lifting theorem.

Almost everything here dates back to the the 1980s or before. The exception is the modularity lifting theorem, which we now state explicitly.

4.2 A modularity lifting theorem

Suppose \(\ell \geq 5\) is a prime, that \(F\) is a totally real field of even degree in which \(\ell \) is unramified, and that \(S\) is a finite set of finite places of \(F\) not dividing \(\ell \). Write \(G_F\) for the absolute Galois group of \(F\).

If \(v\in S\) then let \(F_v\) denote the completion of \(F\) at \(v\), fix an inclusion \(\overline{F}\to \overline{F_v}\), let \(\mathcal{O}_v\) denote the integers of \(F_v\) and \(k(v)\) the residue field. Let \(I_v\subset G_F\) denote the inertia subgroup at \(v\). Local class field theory (or a more elementary approach) gives a map \(I_v\to \mathcal{O}_{F_v}^\times \) and hence a map \(I_v\to k(v)^\times \). Let \(J_v\) denote the kernel of this map.

Let \(R\) be a complete local Noetherian \(\mathbb {Z}_\ell \)-algebra with finite residue field of characteristic \(\ell \). We will be interested in representations \(\rho :G_F\to \operatorname{GL}_2(R)\) with the following four properties.

• \(\det (\rho )\) is the cyclotomic character;

• \(\rho \) is unramified outside \(S\cup \{ \ell \} \);

• If \(v\in S\) then \(\rho (g)\) has trace equal to 2 for all \(g\in J_v\);

• If \(v\mid \ell \) is a place of \(F\) then \(\rho \) is flat at \(v\).

In the last bullet point, “flat” means “projective limit of representations arising from finite flat group schemes”. Let us use the lousy temporary notation “\(S\)-good” to denote representations with these four properties.

Say \(k\) is a finite extension of \(\mathbb {Z}/\ell \mathbb {Z}\) and \(\overline{\rho }:G_F\to \operatorname{GL}_2(k)\) is continuous, absolutely irreducible when restricted to \(F(\zeta _\ell )\), and \(S\)-good. One can check that the functor representing \(S\)-good lifts of \(\overline{\rho }\) is representable.

Right now we are very far from even stating this theorem in Lean.

I am not entirely sure where to find a proof of this in the literature, although it has certainly been known to the experts for some time. Theorem 3.3 of  [ 15 ] comes close, although it assumes that \(\ell \) is totally split in \(F\) rather than just unramified. Another near-reference is Theorem 5.2 of  [ 7 ] , although this assumes the slightly stronger assumption that the image of \(\rho \) contains \(\operatorname{SL}_2(\mathbb {Z}/p\mathbb {Z})\) (however it is well-known to the experts that this can be weakened to give the result we need). One reference for the proof is Richard Taylor’s 2018 Stanford course.

Given this modularity lifting theorem, the strategy to show potential modularity of \(\rho \) is to use Moret–Bailly to find an appropriate totally real field \(F\), an auxiliary prime \(p\), and an auxiliary elliptic curve over \(F\) whose mod \(\ell \) Galois representation is \(\rho \) and whose mod \(p\) Galois representation is induced from a character. By converse theorems (for example) the mod \(p\) Galois representation is associated to an automorphic representation of \(\operatorname{GL}_2/F\) and hence by Jacquet–Langlands it is modular. Now we use the modularity lifting theorem to deduce the modularity of the curve over \(F\) and hence the modularity of the \(\ell \)-torsion.

4.3 Compatible families, and reduction at 3

We now use Khare–Wintenberger to lift \(\rho \) to a potentially modular \(\ell \)-adic Galois representation of conductor 2, and put it into an \(\ell \)-adic family using the Brauer’s theorem trick in [ 1 ] . Finally we look at the 3-adic specialisation of this family. Reducing mod 3 we get a representation which is flat at 3 and tame at 2, so must be reducible because of the techniques introduced in Fontaine’s paper on abelian varieties over \(\mathbb {Z}\) (an irreducible representation would cut out a number field whose discriminant violates the Odlyzko bounds). One can now go on to deduce that the 3-adic representation must be reducible, which contradicts the irreducibility of \(\rho \).

We apologise for the sketchiness of what is here, however at the time of writing it is so far from what we are even able to state in Lean that there seems to be little point right now in fleshing out the argument further. As this document grows, we will add a far more detailed discussion of what is going on here. Note in particular that stating the modularity lifting theorem in Lean is the first target.