You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If Fermat's Last Theorem is false, then there exists a Frey package.
48
48
\end{lemma}
49
-
\begin{proof}\uses{FLT.FreyPackage, FLT.p_ge_5_counterexample_of_not_FermatLastTheorem} By Corollary \ref{p_ge_5_counterexample_of_not_FermatLastTheorem} we may assume that there is a counterexample $a^p+b^p=c^p$ with $p\geq5$ and prime; we now build a Frey package from this data.
49
+
\begin{proof}\uses{FLT.FreyPackage, FLT.p_ge_5_counterexample_of_not_FermatLastTheorem} By Corollary \ref{FLT.p_ge_5_counterexample_of_not_FermatLastTheorem} we may assume that there is a counterexample $a^p+b^p=c^p$ with $p\geq5$ and prime; we now build a Frey package from this data.
50
50
51
51
If the greatest common divisor of $a,b,c$ is $d$ then $a^p+b^p=c^p$ implies $(a/d)^p+(b/d)^p=(c/d)^p$. Dividing through, we can thus assume that no prime divides all of $a,b,c$. Under this assumption we must have that $a,b,c$ are pairwise coprime, as if some prime divides two of the integers $a,b,c$ then by $a^p+b^p=c^p$ and unique factorization it must divide all three of them. In particular we may assume that not all of $a,b,c$ are even, and now reducing modulo~2 shows that precisely one of them must be even.
52
52
@@ -122,21 +122,21 @@ \section{Reduction to two big theorems.}
122
122
Now say Fermat's Last Theorem is false, and hence by Lemma~\ref{FLT.FreyPackage.of_not_FermatLastTheorem} a Frey package $(a,b,c,p)$ exists. Consider the mod $p$ representation of $\GQ$ coming from the $p$-torsion in the Frey curve $Y^2=X(x-a^p)(X+b^p)$ associated to the package. Let's call this representation $\rho$. Is it reducible or irreducible?
123
123
124
124
\begin{theorem}[Mazur]\label{FLT.FreyCurve.Mazur_Frey}\lean{FLT.FreyCurve.Mazur_Frey}\uses{FLT.FreyCurve.mod_p_Galois_representation}\leanok$\rho$ cannot be reducible.\end{theorem}
125
-
\begin{proof}\tangled This follows from a profound result of Mazur \cite{mazur-torsion} from 1979, namely the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact a fair amount of work still needs to be done to deduce the theorem from Mazur's result. We will have more to say about this result later.
125
+
\begin{proof}\uses{Frey_curve_irreducible}\tangled This follows from a profound result of Mazur \cite{mazur-torsion} from 1979, namely the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact a fair amount of work still needs to be done to deduce the theorem from Mazur's result. We will have more to say about this result later.
126
126
\end{proof}
127
127
128
-
\begin{theorem}[Wiles,Taylor--Wiles, Ribet,\ldots]\label{FLT.FreyCurve.Wiles_Frey}\lean{FLT.FreyCurve.Wiles_Frey}\uses{FLT.FreyCurve.mod_p_Galois_representation}\leanok$\rho$ cannot be irreducible either.\end{theorem}
129
-
\begin{proof}\uses{Frey_mod_p_Galois_representation}\tangled This is the main content of Wiles' magnum opus. We omit the argument for now, although later on in this project we will have a lot to say about a proof of this.
128
+
\begin{theorem}[Wiles,Taylor--Wiles, Ribet,\ldots]\label{FLT.FreyCurve.Wiles_Frey}\lean{FLT.FreyCurve.Wiles_Frey}\uses{FLT.FreyCurve.mod_p_Galois_representation, modularity_lifting_theorem}\leanok$\rho$ cannot be irreducible either.\end{theorem}
129
+
\begin{proof}\uses{Frey_mod_p_Galois_representation, frey_curve_hardly_ramified}\tangled This is the main content of Wiles' magnum opus. We omit the argument for now, although later on in this project we will have a lot to say about a proof of this.
130
130
\end{proof}
131
131
132
132
\begin{corollary}\label{FLT.Frey_package.false}\lean{FLT.Frey_package.false}\uses{FLT.FreyCurve.Mazur_Frey, FLT.FreyCurve.Wiles_Frey}\leanok There is no Frey package.\end{corollary}
133
-
\begin{proof}\leanok Follows immediately from the previous two theorems~\ref{Mazur_on_Frey_curve} and~\ref{Wiles_on_Frey_curve}.\end{proof}
133
+
\begin{proof}\leanok Follows immediately from the previous two theorems~\ref{FLT.FreyCurve.Mazur_Frey} and~\ref{FLT.FreyCurve.Wiles_Frey}.\end{proof}
134
134
135
135
We deduce
136
136
137
137
\begin{corollary}\label{FLT}\lean{Wiles_Taylor_Wiles}\uses{FLT.Frey_package.false, FLT.FreyPackage.of_not_FermatLastTheorem}\leanok Fermat's Last Theorem is true.\end{corollary}
138
138
\begin{proof}\leanok
139
-
Indeed, if Fermat's Last Theorem is false then there is a Frey package $(a,b,c,p)$ by~\ref{Frey_package_of_FLT_counterex}, contradicting Corollary~\ref{no_Frey_package}.
139
+
Indeed, if Fermat's Last Theorem is false then there is a Frey package $(a,b,c,p)$ by~\ref{FLT.FreyPackage.of_not_FermatLastTheorem}, contradicting Corollary~\ref{FLT.Frey_package.false}.
140
140
\end{proof}
141
141
142
-
The structure of the rest of this document is as follows. In Chapter 3 we develop some of the basic theory of elliptic curves and the Galois representations attached to their $p$-torsion subgroups. We then apply this theory to the Frey curve, deducing in particular how Mazur's result on torsion subgroups of elliptic curves implies Theorem~\ref{Mazur_on_Frey_curve}, the assertion that $\rho$ cannot be reducible. In Chapter~\ref{ch_overview} we give a high-level overview of our strategy to prove that $\rho$ cannot be irreducible, which diverges from the original approach taken by Wiles; one key difference is that we work with the $p$-torsion directly rather than switching to the 3-torsion. We also give a precise statement of the modularity lifting theorem which we will use. Finally, in Chapter~\ref{ch_bestiary} we give a collection of theorem statements which we shall need in order to push our strategy through. All of these results were known in the 1980s or before. This chapter is incoherent in the sense that it is just a big list of apparently unrelated results. As our exposition of the proof expands, the results of this chapter will slowly move to more appropriate places. The chapter is merely there to give some kind of idea of the magnitude of the project.
142
+
The structure of the rest of this (highly incomplete, for now) document is as follows. In Chapter 3 we develop some of the basic theory of elliptic curves and the Galois representations attached to their $p$-torsion subgroups. We then apply this theory to the Frey curve, deducing in particular how Mazur's result on torsion subgroups of elliptic curves implies Theorem~\ref{FLT.FreyCurve.Mazur_Frey}, the assertion that $\rho$ cannot be reducible. In Chapter~\ref{ch_overview} we give a high-level overview of our strategy to prove that $\rho$ cannot be irreducible, which diverges from the original approach taken by Wiles; one key difference is that we work with the $p$-torsion directly rather than switching to the 3-torsion. We also give a precise statement of the modularity lifting theorem which we will use. Finally, in Chapter~\ref{ch_bestiary} we give a collection of theorem statements which we shall need in order to push our strategy through. All of these results were known in the 1980s or before. This chapter is incoherent in the sense that it is just a big list of apparently unrelated results. As our exposition of the proof expands, the results of this chapter will slowly move to more appropriate places. The chapter is merely there to give some kind of idea of the magnitude of the project.
This follows from the previous group-theoretic lemma~\ref{group_theory_lemma} and
39
-
theorem~\ref{Elliptic_curve_n_torsion_size}.
39
+
theorem~\ref{EllipticCurve.torsion_card}.
40
40
\end{proof}
41
41
42
42
We saw in section~\ref{twopointfour} that if $E$ is an elliptic curve over a field $k$ and if $k^{\sep}$ is a separable closure of~$k$, then the group $\Gal(k^{\sep}/k)$ acts on $E(k^{\sep})[n]$. Now let $n$ be a positive integer which is nonzero in $k$. We have just seen that $E(k^{\sep})[n]$ is isomorphic to $(\Z/n\Z)^2$, and it inherits an action of $\Gal(k^{\sep}/k)$. If we fix an isomorphism $E(k^{\sep})[n]\cong(\Z/n\Z)^2$ then we get a representation $\Gal(k^{\sep}/k)\to\GL_2(\Z/n\Z)$. A fundamental fact about this Galois representation is that its determinant is the cyclotomic character.
Everything here is from the 20th century, and most of it is from the 1980s or before.
34
-
The exception is the modularity lifting theorem, which we state explicitly here.
34
+
Almost verything here dates back to the the 1980s or before.
35
+
The exception is the modularity lifting theorem, which we now state explicitly.
35
36
36
-
**TODO** state modularity lifting theorem.
37
+
\section{A modularity lifting theorem}
38
+
39
+
Suppose $\ell\geq5$ is a prime, that $F$ is a totally real field of even degree in which $\ell$
40
+
is unramified, and that~$S$ is a finite set of finite places of~$F$ not dividing~$\ell$. Write
41
+
$G_F$ for the absolute Galois group of~$F$.
42
+
43
+
If $v\in S$ then let $F_v$ denote the completion of~$F$ at~$v$, fix an inclusion $\overline{F}\to\overline{F_v}$,
44
+
let $\calO_v$ denote the integers of $F_v$ and $k(v)$ the residue field. Let $I_v\subset G_F$ denote the inertia
45
+
subgroup at~$v$. Local class field theory (or a more elementary approach) gives a map $I_v\to\calO_{F_v}^\times$
46
+
and hence a map $I_v\to k(v)^\times$. Let $J_v$ denote the kernel of this map.
47
+
48
+
Let $R$ be a complete local Noetherian $\Z_\ell$-algebra with finite residue field of characteristic $\ell$.
49
+
We will be interested in representations $\rho:G_F\to\GL_2(R)$ with the following four properties.
50
+
\begin{itemize}
51
+
\item$\det(\rho)$ is the cyclotomic character;
52
+
\item$\rho$ is unramified outside $S\cup\{\ell\}$;
53
+
\item If $v\in S$ then $\rho(g)$ has trace equal to~2 for all $g\in J_v$;
54
+
\item If $v\mid\ell$ is a place of $F$ then $\rho$ is flat at~$v$.
55
+
\end{itemize}
56
+
57
+
In the last bullet point, ``flat'' means ``projective limit of representations arising from
58
+
finite flat group schemes''. Let us use the lousy temporary notation ``$S$-good'' to denote
59
+
representations with these four properties.
60
+
61
+
Say $k$ is a finite extension of $\Z/\ell\Z$ and $\rhobar:G_F\to\GL_2(k)$ is continuous,
62
+
absolutely irreducible when restricted to $F(\zeta_\ell)$, and $S$-good. One can check
63
+
that the functor representing $S$-good lifts of $\rhobar$ is representable.
64
+
65
+
\begin{theorem}\label{modularity_lifting_theorem}
66
+
If $\rhobar$ is modular of level $\Gamma_1(S)$ then any $S$-good $\ell$-adic lift
67
+
$\rho:G_F\to\GL_2(\calO)$ is also modular of level $\Gamma_1(S)$.
68
+
\end{theorem}
69
+
70
+
Right now we are very far from even stating this theorem in Lean.
37
71
38
72
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~\cite{taylor-mero-cont} comes close, although it assumes that $\ell$ is totally split in $F$ rather than just unramified. Another near-reference is Theorem~5.2 of~\cite{toby-modularity}, although this assumes
39
73
the slightly stronger assumption that the image of $\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 \href{https://math.berkeley.edu/~fengt/249A_2018.pdf}{Richard Taylor's 2018 Stanford course}.
40
74
41
-
Given the 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 auxilary prime $p$, and an auxiliary elliptic curve over $F$ whose mod $\ell$ Galois representation is $\rho$ and whose
75
+
\begin{proof} (Sketch)
76
+
77
+
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
78
+
of the image of the base change construction; this seems to need a multiplicity one result, which (because of our
79
+
definition of ``modular'') will need Jacquet--Langlands as well.
80
+
81
+
In the minimal case, the argument is the usual Taylor--Wiles trick, using refinements due to Kisin and others.
82
+
\end{proof}
83
+
84
+
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 auxilary prime $p$, and an auxiliary elliptic curve over $F$ whose mod $\ell$ Galois representation is $\rho$ and whose
42
85
mod $p$ Galois representation is induced from a character. By converse theorems (for example)
43
86
the mod $p$ Galois representation is associated to an automorphic representation of
44
87
$\GL_2/F$ and hence by Jacquet--Langlands it is modular. Now we use the
@@ -57,8 +100,7 @@ \section{Compatible families, and reduction at 3}
57
100
One can now go on to deduce that the 3-adic representation must be reducible, which
58
101
contradicts the irreducibility of $\rho$.
59
102
60
-
As this document grows, we will add a far more detailed discussion of
61
-
what is going on here.
103
+
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 \emph{state} in Lean that there seems to be little point in fleshing out the argument further. As this document grows, we will add a far more detailed discussion of what is going on here.
Copy file name to clipboardexpand all lines: blueprint/src/chapter/chtopbestiary.tex
+2-2
Original file line number
Diff line number
Diff line change
@@ -1,6 +1,6 @@
1
-
\chapter{Appendix: A collection of results which are needed in the proof.}
1
+
\chapter{Appendix: A collection of results which are needed in the proof.}\label{ch_bestiary}
2
2
3
-
In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face.
3
+
In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face.
0 commit comments