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
-- The way to turn this node green is to port that work to mathlib so we can use it here.
54
+
-- This is proved in the FLT-regular project (https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698)
55
+
-- and the FLT3 project (https://github.com/riccardobrasca/flt3).
56
+
-- The way to turn this node green is to port this latter one to mathlib so we can use it here.
Copy file name to clipboardexpand all lines: blueprint/src/chapter/ch02reductions.tex
+15-12
Original file line number
Diff line number
Diff line change
@@ -1,7 +1,7 @@
1
-
\chapter{First reductions of the problem.}
1
+
\chapter{First reductions of the problem}
2
2
3
3
\section{Overview}
4
-
The proof of Fermat's Last Theorem is by contradiction. We assume that we have a counterexample $a^n+b^n=c^n$, and manipulate it until it satsfies the axioms of a ``Frey package''. From the Frey package we build a Frey curve -- an elliptic curve defined over the rationals. We then look at a certain representation of a Galois group coming from this elliptic curve, and finally using two very deep and independent theorems (one due to Mazur, the other due to Wiles) we show that this representation is neither reducible or irreducible, a contradiction.
4
+
The proof of Fermat's Last Theorem is by contradiction. We assume that we have a counterexample $a^n+b^n=c^n$, and manipulate it until it satisfies the axioms of a ``Frey package''. From the Frey package we build a Frey curve -- an elliptic curve defined over the rationals. We then look at a certain representation of a Galois group coming from this elliptic curve, and finally using two very deep and independent theorems (one due to Mazur, the other due to Wiles) we show that this representation is neither reducible or irreducible, a contradiction.
5
5
6
6
\section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
7
7
@@ -28,7 +28,10 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
28
28
There are no solutions in positive integers to $a^3+b^3=c^3$.
29
29
\end{lemma}
30
30
\begin{proof}
31
-
The proof has been formalised in Lean in the FLT-regular project \href{https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698}{\underline{here}}. To get this node green, the proof (or another proof) needs to be upstreamed to mathlib. This is currently work in progress by a team from the Lean For the Curious Mathematician conference held in Luminy in March 2024.
31
+
A proof has been formalised in Lean in the FLT-regular project \href{https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698}{\underline{here}}.
32
+
Another proof has been formalised in Lean in the FLT3 project \href{https://github.com/riccardobrasca/flt3}{\underline{here}} by a team from the Lean For the Curious Mathematician conference held in Luminy in March 2024
33
+
(its dependency graph can be visualised \href{https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html}{\underline{here}}).
34
+
To get this node green, this latter proof needs to be upstreamed to mathlib. This is currently work in progress by the same team.
32
35
\end{proof}
33
36
34
37
\begin{corollary}\label{FLT.p_ge_5_counterexample_of_not_FermatLastTheorem}\lean{FLT.p_ge_5_counterexample_of_not_FermatLastTheorem}\leanok If there is a counterexample to Fermat's Last Theorem, then there is a counterexample $a^p+b^p=c^p$ with $p$ prime and $p\geq5$.
@@ -47,9 +50,9 @@ \section{Frey packages}
47
50
If Fermat's Last Theorem is false, then there exists a Frey package.
48
51
\end{lemma}
49
52
\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
-
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
-
53
+
54
+
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.
55
+
53
56
Next we show that we can find a counterexample with $b$ even. If $a$ is the even one then we can just switch $a$ and $b$. If $c$ is the even one then we can replace $c$ by $-b$ and $b$ by $-c$ (using that $p$ is odd).
54
57
55
58
The last thing to ensure is that $a$ is 3 mod~4. Because $b$ is even, we know that $a$ is odd, so it is either~1 or~3 mod~4. If $a$ is 3 mod~4 then we are home; if however $a$ is 1 mod~4 we replace $a,b,c$ by their negatives and this is the Frey package we seek.
@@ -63,7 +66,7 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
63
66
64
67
The group structure behaves well under change of field.
65
68
66
-
\begin{lemma}\label{EllipticCurve.Points.map}\lean{EllipticCurve.Points.map}\leanok If $E$ is an elliptic curve over a field $k$, and if $K$ and $L$ are two fields which are $k$-algebras, and if $f:K\to L$ is a $k$-algebra homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive group homomorphism.
69
+
\begin{lemma}\label{EllipticCurve.Points.map}\lean{EllipticCurve.Points.map}\leanok If $E$ is an elliptic curve over a field $k$, and if $K$ and $L$ are two fields which are $k$-algebras, and if $f:K\to L$ is a $k$-algebra homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive group homomorphism.
67
70
\end{lemma}
68
71
\begin{proof} The equations defining the group law are ratios of polynomials with coefficients in $k$, and such things behave well under $k$-algebra homomorphisms.
69
72
\end{proof}
@@ -85,22 +88,22 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
85
88
\begin{proof} Another easy calculation.
86
89
\end{proof}
87
90
88
-
Thus if $fK\to L$ is an isomorphism of fields, the induced map $E(K)\to E(L)$ is an isomorphism of groups, with the inverse isomorphism being the map $E(L)\to E(K)$ induced by $f^{-1}$. This construction thus gives us an action of the multiplicative group $\Aut_k(K)$ of automorphisms of the field $K$ on the additive abelian group $E(K)$.
89
-
91
+
Thus if $f:K\to L$ is an isomorphism of fields, the induced map $E(K)\to E(L)$ is an isomorphism of groups, with the inverse isomorphism being the map $E(L)\to E(K)$ induced by $f^{-1}$. This construction thus gives us an action of the multiplicative group $\Aut_k(K)$ of automorphisms of the field $K$ on the additive abelian group $E(K)$.
If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a $k$-algebra,
92
95
then the group of $k$-automorphisms of $K$ acts on the additive abelian group $E(K)$.
93
96
\end{definition}
94
97
In particular, if $\Qbar$ denotes an algebraic closure of the rationals (for example, the algebraic numbers in $\bbC$) and if $\GQ$ denotes the group of field isomorphisms $\Qbar\to\Qbar$, then for any elliptic curve $E$ over $\Q$ we have an action of $\GQ$ on the additive abelian group $E(\Qbar)$.
95
98
96
-
We need a variant of this construction where we only consider the $n$-torsion of the curve, for $n$ a positive integer. Recall that if $A$ is any additive abelian group, and if $n$ is a positive integer, then we can consider the subgroup $A[n]$ of elements $a$ such that $na=0$. If a group~$G$ acts on $A$ via additive group isomorphisms, then there will be an induced action of~$G$ on $A[n]$.
99
+
We need a variant of this construction where we only consider the $n$-torsion of the curve, for $n$ a positive integer. Recall that if $A$ is any additive abelian group, and if $n$ is a positive integer, then we can consider the subgroup $A[n]$ of elements $a$ such that $na=0$. If a group~$G$ acts on $A$ via additive group isomorphisms, then there will be an induced action of~$G$ on $A[n]$.
If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a $k$-algebra,
100
103
and if $n$ is a natural number, hen the group of $k$-automorphisms of $K$ acts on the additive abelian group $E(K)[n]$ of $n$-torsion points on the curve.
101
104
\end{definition}
102
105
103
-
If furthermore $n=p$ is prime, then $A[p]$ is naturally a vector space over the field $\Z/p\Z$, and thus it inherits the stucture of a mod $p$ representation of $G$. Applying this to the above situation, we deduce that if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to the curve $E$.
106
+
If furthermore $n=p$ is prime, then $A[p]$ is naturally a vector space over the field $\Z/p\Z$, and thus it inherits the structure of a mod $p$ representation of $G$. Applying this to the above situation, we deduce that if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to the curve $E$.
104
107
105
108
In the next section we apply this theory to an elliptic curve coming from a counterexample to Fermat's Last theorem.
106
109
@@ -114,7 +117,7 @@ \section{The Frey curve}
114
117
Given a Frey package $(a,b,c,p)$ with corresponding Frey curve $E$, the mod $p$ Galois representation associated to this package is the representation of $\GQ$ on $E(\Qbar)[p].$ Frey's observation is that this mod $p$ Galois representation has some very surprising properties. We will make this remark more explicit in the next chapter. Here we shall show how these properties can be used to finish the job.
115
118
116
119
\section{Reduction to two big theorems.}
117
-
120
+
118
121
Recall that a representation of a group $G$ on a vector space $W$ is said to be \emph{irreducible} if there are precisely two $G$-stable subspaces of $W$, namely $0$ and $W$. The representation is said to be \emph{reducible} otherwise.
119
122
120
123
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?
In the minimal case, the argument is the usual Taylor--Wiles trick, using refinements due to Kisin and others.
83
83
\end{proof}
84
84
85
-
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
85
+
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
86
86
mod $p$ Galois representation is induced from a character. By converse theorems (for example)
87
87
the mod $p$ Galois representation is associated to an automorphic representation of
88
88
$\GL_2/F$ and hence by Jacquet--Langlands it is modular. Now we use the
Copy file name to clipboardexpand all lines: blueprint/src/chapter/chtopbestiary.tex
+3-3
Original file line number
Diff line number
Diff line change
@@ -9,7 +9,7 @@ \section{Results from class field theory}
9
9
Let $K$ be a finite extension of $\Q_p$. We write $\widehat{\Z}$ for the profinite completion of $\Z$; it is isomorphic to $\prod_p\Z_p$ where $\Z_p$ is the $p$-adic integers and the product is over all primes.
10
10
11
11
\begin{theorem}\label{maximal_unramified_extension_of_p-adic_field}\notready The maximal unramified extension $K^{un}$ in a given algebraic closure of $K$
12
-
is Galois over $K$ with Galois group ``canonically'' isomorphic to $\widehat{\Z}$ in two ways; one of these two isomorphisms identifies $1\in\widehat{\Z}$ with an arithmetic Frobenius (the endomorphism inducing $x\mapsto x^q$ on the residue field of $K^{un}$, where $q$ is the size of the residue field of $K$). The other identifies 1 with geometric Frobenius (defined to be the inverse of arithematic Frobenius).
12
+
is Galois over $K$ with Galois group ``canonically'' isomorphic to $\widehat{\Z}$ in two ways; one of these two isomorphisms identifies $1\in\widehat{\Z}$ with an arithmetic Frobenius (the endomorphism inducing $x\mapsto x^q$ on the residue field of $K^{un}$, where $q$ is the size of the residue field of $K$). The other identifies 1 with geometric Frobenius (defined to be the inverse of arithmetic Frobenius).
13
13
\end{theorem}
14
14
15
15
It is impossible to say which of the two canonical isomorphisms is ``the most canonical''; people working in different areas make different choices in order to locally minimise the number of minus signs in their results.
@@ -158,7 +158,7 @@ \section{Automorphic forms and representations}
158
158
\item$\phi$ is locally constant on $G(\A_N^f)$ and $C^\infty$ on $G(N_\infty)$. In other words, for every $g_\infty$, $\phi(-,g_\infty)$ is locally constant, and for every $g_f$, $\phi(g_f,-)$ is smooth.
159
159
\item$\phi$ is left-invariant under $G(N)$;
160
160
\item$\phi$ is right-$U_\infty$-finite (that is, the space spanned by $x\mapsto\phi(xu)$ as $u$ varies over $U_\infty$ is finite-dimensional);
161
-
\item$\phi$ is right $K_f$-finite, where $K_f$ is one (or equivalentally all) compact open subgroups of $G(\A_N^f)$;
161
+
\item$\phi$ is right $K_f$-finite, where $K_f$ is one (or equivalently all) compact open subgroups of $G(\A_N^f)$;
162
162
\item$\phi$ is $\mathcal{z}$-finite, where $\mathcal{z}$ is the centre of the universal enveloping algebra of the Lie algebra of $G(N_\infty)$, acting via differential operators. Equivalently $\phi$ is annihiliated by a finite index ideal of this centre, so morally $\phi$ satisfies lots of differential equations of a certain type;
163
163
\item For all $g_f$, the function $g_\infty\mapsto\phi(g_f g\infty)$ is slowly-increasing in the sense above.
We have already mentioned Mazur's Theorem on torsion subgroups of elliptic curves (theorem~\cite{mazur}).
220
-
The proof of this is 100 pages of a subtle analysis of the bad reduction of modular curves and the consquences of this on their Jacobians.
220
+
The proof of this is 100 pages of a subtle analysis of the bad reduction of modular curves and the consequences of this on their Jacobians.
221
221
222
222
Talking of modular curves, we also need the existence of Shimura curves and surfaces over totally real fields~$F$ (of degree greater than~2, so always compact). The curves are "modeles \'etranges" in the sense of Deligne, so we also need moduli spaces of unitary Shimura varieties over CM extensions. We need to decompose the first and second etale cohomology groups of these varieties into Galois representations, by understanding them
0 commit comments