attempt to get graph perfect

blueprint/src/chapter/introduction.tex

@@ -42,7 +42,7 @@ \section{Frey packages.}
 
 Our next reduction is as follows:
 
-\begin{lemma}\label{FreyPackage_of_FLT}\lean{FLT.Frey_package.of_not_FermatLastTheorem}\uses{Frey_package, WLOG_p_ge_5}\leanok
+\begin{lemma}\label{Frey_package_of_FLT_counterex}\lean{FLT.FreyPackage.of_not_FermatLastTheorem}\uses{Frey_package, WLOG_p_ge_5}\leanok
   If Fermat's Last Theorem is false, then there exists a Frey package.
 \end{lemma}
 \begin{proof} By \ref{WLOG_p_ge_5} we may assume that there is a counterexample $x^p+y^p=z^p$ with $p\geq 5$ and prime; we now manipulate this counterexample until we get a Frey Package.
@@ -82,14 +82,14 @@ \section{Galois representations and elliptic curves}
 
 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?
 
-\begin{theorem}[Mazur]\label{Mazur_on_Frey_curve}\lean{FLT.FreyCurve.Mazur_Frey}\uses{Frey_curve}\leanok $\rho$ cannot be reducible.\end{theorem}
+\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
 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}
 
-\begin{theorem}[Wiles,Taylor--Wiles]\label{Wiles_on_Frey_curve}\lean{FLT.FreyCurve.Wiles_Frey}\uses{Frey_curve}\leanok $\rho$ cannot be irreducible either.\end{theorem}
+\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.
 \end{proof}
 
@@ -98,7 +98,7 @@ \section{Galois representations and elliptic curves}
 
 These two theorems together give the contraction required. We deduce
 
-\begin{corollary}\label{FLT}\lean{Wiles_Taylor_Wiles}\uses{no_Frey_package}\leanok Fermat's Last Theorem is true.\end{corollary}
+\begin{corollary}\label{FLT}\lean{Wiles_Taylor_Wiles}\uses{no_Frey_package, Frey_package_of_FLT_counterex}\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{FreyPackage_of_FLT}, and the corresponding Galois representation $\rho$ on the $p$-torsion of the Frey curve is neither reducible nor irreducible, a contradiction.
 \end{proof}