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 : \GQ \to \GL_2(\Z/\ell\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 \Q.
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 and at all infinite places". Such a quaternion algebra only
exists if F has even degree, hence the restriction in our definition of
modularity. We can furthermore even demand that the infinity type of the form
is trivial (the analogue in this setting of classical weight 2 forms), 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 \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 (Moret-Bailly, 1989
) on points on curves with prescribed local behaviour;Laurent Moret-Bailly (1989). “Groupes de Picard et problèmes de Skolem. I, II”. Annales scientifiques de l'École Normale Supérieure.22 2pp. 161–179. -
several nontrivial results in global class field theory;
-
the Jacquet--Langlands correspondence;
-
The assertion that irreducible
2-dimensional modprepresentations induced from a character are modular (this follows from converse theorems); -
A modularity lifting theorem.
Almost everything here dates back to 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 \calO_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 \calO_{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 \Z_\ell-algebra with finite residue
field of characteristic \ell. We will be interested in representations
\rho : G_F \to \GL_2(R) with the following four properties.
-
\det(\rho)is the cyclotomic character; -
\rhois unramified outsideS \cup \{\ell\}; -
If
v \in Sthen\rho(g)has trace equal to2for allg \in J_v; -
If
v \mid \ellis a place ofFthen\rhois flat atv.
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 \Z/\ell\Z and
\rhobar : G_F \to \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 \rhobar is representable.
- No associated Lean code or declarations.
Theorem 14.10
Theorem 14.9
Let
If
If
If
The natural map
Definition 14.22
An irreducible admissible
Theorem 14.26
A cuspidal automorphic representation is an irreducible
Definition 14.22
Definition 14.23
Definition 14.28
Given an automorphic representation
Let
If S be a finite set of places of a number field K. For each v \in S
let L_v/K_v be a finite Galois extension. Then there is a finite solvable
Galois extension L/K such that if w is a place of L dividing v \in S,
then L_w/K_v is isomorphic to L_v/K_v as a K_v-algebra. Moreover, if
K^{\avoid}/K is any finite extension then L can be chosen linearly
disjoint from K^{\avoid}.M is torsion then H^i(G_K,M)=0 if i>2.H^2(G_K,\mu_n) is canonically isomorphic to \Z/n\Z.\mu=\bigcup_{n\geq1}\mu_n and M':=\Hom(M,\mu) is the dual of M,
then for 0\leq i\leq 2 the cup-product pairing
H^i(G_K,M)\times H^{2-i}(G_K,M')\to H^2(G_K,\mu)=\Q/\Z is perfect.h^i(M) denotes the order of H^i(G_K,M), then
h^0(M)-h^1(M)+h^2(M)=0.L \otimes_K \A_{A,K}^\infty \to \A_{B,L}^\infty is an
isomorphism.
Theorem 9.13
Definition 9.22
Theorem 9.27
Corollary 9.19(G(\A_N^f)\times U_\infty,\mathfrak{g})-module is a
restricted tensor product of irreducible representations \pi_v of G(N_v)
as v runs through the finite places of N, tensored with a tensor product of
irreducible (\mathfrak{g}_v,U_{\infty,v})-modules as v runs through the
infinite places of N. The representations \pi_v are unramified for all but
finitely many v.(G(\A_N^f)\times U_\infty,\mathfrak{g})-module isomorphic to an irreducible
summand of the space of cusp forms.\pi for an inner form of \GL_2 over a
totally real field and with reflex field E, such that \pi is weight 2
discrete series at every infinite place, there exists a compatible family of
2-dimensional Galois representations associated to \pi, with S the
places at which \pi is ramified and F_{\mathfrak p}(X) the monic
polynomial with roots the two Satake parameters for \pi at \mathfrak p.K^{\avoid}/K be a Galois extension of number fields. Suppose also that
S is a finite set of places of K, and for each v\in S let
L_v/K_v be a finite Galois extension. Suppose also that T/K is a
smooth, geometrically connected curve and that for each v\in S we are given
a nonempty, \operatorname{Gal}(L_v/K_v)-invariant open subset
\Omega_v\subseteq T(L_v). Then there is a finite Galois extension L/K and
a point P\in T(L) with the prescribed local behavior.M is finite then the cohomology groups H^i(G_K,M) are all finite.\rhobar is modular of level \Gamma_1(S) and
\rho : G_F \to \GL_2(\calO) is an S-good lift of \rhobar to \calO, the
integers of a finite extension of \Q_\ell, then \rho is also modular of
level \Gamma_1(S).
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 (Taylor, 2006\ell is totally split in F rather than just unramified. Another
near-reference is Theorem 5.2 of (Gee, 2006\rho
contains \SL_2(\Z/p\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.
Sketch.
The proof is a two-stage procedure and has a nontrivial analytic input. First
one uses the Skinner--Wiles trick to reduce to the "minimal case", and this
needs cyclic base change for \GL(2) and also a characterisation of the image
of the base change construction; this seems to need a multiplicity one result,
which (because of our definition of "modular") will need Jacquet--Langlands as
well.
In the minimal case, the argument is the usual Taylor--Wiles trick, using refinements due to Kisin and others.
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 \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
(Barnet-Lamb et al., 20143-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 \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.