checkdecls now working

Author: kbuzzard

blueprint/src/chapter/ch02reductions.tex

@@ -87,15 +87,15 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
 
  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)$. 
 
-\begin{definition}\label{EllipticCurve.galoisRepresentation}\lean{EllipticCurve.GaloisRepresentation}\uses{EllipticCurve.Points.map_id,EllipticCurve.Points.map_comp}
+\begin{definition}\label{EllipticCurve.galoisRepresentation}\lean{EllipticCurve.galoisRepresentation}\uses{EllipticCurve.Points.map_id,EllipticCurve.Points.map_comp}
   If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a $k$-algebra,
   then the group of $k$-automorphisms of $K$ acts on the additive abelian group $E(K)$.
 \end{definition}
  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)$.
 
 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]$. 
 
-\begin{definition}\label{EllipticCurve.torsionGaloisRepresentation}\lean{EllipticCurve.GaloisRepresentation}\uses{EllipticCurve.galoisRepresentation}
+\begin{definition}\label{EllipticCurve.torsionGaloisRepresentation}\lean{EllipticCurve.torsionGaloisRepresentation}\uses{EllipticCurve.galoisRepresentation}
   If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a $k$-algebra,
   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.
 \end{definition}
@@ -106,37 +106,35 @@ \section{Galois representations and elliptic curves}\label{twopointfour}
 
 \section{The Frey curve}
 
-\begin{definition}[Frey]\label{FLT.FreyCurve}\lean{FLT.FreyCurve}\uses{FLT.FreyPackage}\discussion{21}
+\begin{definition}[Frey]\label{FLT.FreyCurve}\lean{FLT.FreyPackage.FreyCurve}\uses{FLT.FreyPackage}\discussion{21}
   Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellegouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p).$\end{definition}
 
 Note that the roots of the cubic $X(X-a^p)(X+b^p)$ are distinct because $a,b,c$ are nonzero and $a^p+b^p=c^p$.
 
-\begin{definition}[mod $p$ Galois representation attached to a Frey package]\label{FLT.FreyCurve.mod_p_Galois_representation}\lean{FLT.FreyCurve.mod_p_Galois_representation}\uses{FLT.FreyCurve,EllipticCurve.torsionGaloisRepresentation} 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].$\end{definition}
-
-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.
+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.
 
 \section{Reduction to two big theorems.}
 
 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.
 
 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?
 
-\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}
+\begin{theorem}[Mazur]\label{FLT.Mazur_Frey}\lean{FLT.Mazur_Frey}\uses{FLT.FreyCurve}\leanok $\rho$ cannot be reducible.\end{theorem}
 \begin{proof}\uses{Frey_curve_irreducible}\notready 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.
 \end{proof}
 
-\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}
+\begin{theorem}[Wiles,Taylor--Wiles, Ribet,\ldots]\label{FLT.Wiles_Frey}\lean{FLT.Wiles_Frey}\uses{FLT.FreyCurve}\leanok $\rho$ cannot be irreducible either.\end{theorem}
 \begin{proof}\uses{modularity_lifting_theorem,frey_curve_hardly_ramified}\notready 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.
 \end{proof}
 
-\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}
-\begin{proof}\leanok Follows immediately from the previous two theorems~\ref{FLT.FreyCurve.Mazur_Frey} and~\ref{FLT.FreyCurve.Wiles_Frey}.\end{proof}
+\begin{corollary}\label{FLT.FreyPackage.false}\lean{FLT.FreyPackage.false}\uses{FLT.Mazur_Frey, FLT.Wiles_Frey}\leanok There is no Frey package.\end{corollary}
+\begin{proof}\leanok Follows immediately from the previous two theorems~\ref{FLT.Mazur_Frey} and~\ref{FLT.Wiles_Frey}.\end{proof}
 
 We deduce
 
-\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}
+\begin{corollary}\label{FLT}\lean{FLT.Wiles_Taylor_Wiles}\uses{FLT.FreyPackage.false, FLT.FreyPackage.of_not_FermatLastTheorem}\leanok Fermat's Last Theorem is true.\end{corollary}
 \begin{proof}\leanok
-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}.
+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.FreyPackage.false}.
 \end{proof}
 
-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.
+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.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.

blueprint/src/chapter/ch03frey.tex

@@ -29,7 +29,7 @@ \section{The arithmetic of elliptic curves}
   with $a_i\mid a_{i+1}$ (this is possible by the structure theorem for finite abelian groups), and then to apply our hypothesis firstly with $d=a_1$ to deduce $t=r$ and then with $d=a_t$ to deduce $a_1=a_t$.
 \end{proof}
 
-\begin{corollary}\label{Elliptic_curve_n_torsion_2d}\lean{EllipticCurve.n_torsion_rank}
+\begin{corollary}\label{Elliptic_curve_n_torsion_2d}\lean{EllipticCurve.n_torsion_dimension}
   Let $n$ be a positive integer, let $F$ be a separably closed
   field with $n$ nonzero in $F$, and let $E$ be an elliptic curve over $F$. Then the $n$-torsion $E(F)[n]$ 
   in the $F$-points of $E$ is a finite group isomorphic to $(\Z/n\Z)^2$.