typos

blueprint/src/chapter/introduction.tex

@@ -76,18 +76,20 @@ \section{Galois representations and elliptic curves}
 Note that the roots of the cubic $X(X-a^p)(X+b^p)$ are distinct because $a,b,c$ are nonzero, and thus the Frey curve is an
 elliptic curve over $\Q$.
 
-\begin{definition}[mod $p$ Galois representation attached to a Frey package]\label{Frey_mod_p_Galois_representation}\lean{FLT.FreyCurve.mod_p_Galois_representation}\uses{Frey_curve} 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}
+\begin{definition}[mod $p$ Galois representation attached to a Frey package]\label{Frey_mod_p_Galois_representation}\lean{FLT.FreyCurve.mod_p_Galois_representation}\uses{Frey_curve} 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}
 
 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 a Frey package $(a,b,c,p)$ exists. and consider the corresponding mod $p$ representation of $\GQ$ coming from the $p$-torsion in the Frey curve $Y^2=X(x-a^p)(X+b^p)$. Let's call this representation $\rho$. Is this representation reducible or irreducible?
+Now say Fermat's Last Theorem is false, and hence by Lemma~\ref{Frey_package_of_FLT_counterex} 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{Mazur_on_Frey_curve}\lean{FLT.FreyCurve.Mazur_Frey}\uses{Frey_mod_p_Galois_representation}\leanok $\rho$ cannot be reducible.\end{theorem}
-\begin{proof}\tangled This follows from a profound result of Mazur from 1979 {\bf todo reference}, which boils down to the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact some work still needs to be done to deduce the theorem from Mazur's result. We omit the argument for now -- it is explained in Proposition~6 of~\cite{serreconj}. The reduction to Mazur's theorem
+\begin{proof}\tangled This follows from a profound result of Mazur \cite{mazur} from 1979, which boils down to the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact some work still needs to be done to deduce the theorem from Mazur's result. We omit the argument for now -- it is explained in Proposition~6 of~\cite{serreconj}. The reduction to Mazur's theorem
 needs the theory of the Tate curve (concrete p-adic uniformisation of elliptic curves) and also some of the theory of finite flat group schemes (or the theory of the canonical subgroup), so in particular even the reduction to Mazur's theorem is a lot of hard work.
 Mazur's theorem itself is of course way more difficult, and right now nobody is working on a formalisation (it would be a substantial
 project in itself).
 \end{proof}
+{\bf TODO two rferences above}
 
 \begin{theorem}[Wiles,Taylor--Wiles]\label{Wiles_on_Frey_curve}\lean{FLT.FreyCurve.Wiles_Frey}\uses{Frey_mod_p_Galois_representation}\leanok $\rho$ cannot be irreducible either.\end{theorem}
 \begin{proof}\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.