fix arrows

blueprint/src/chapter/reductions.tex

@@ -27,9 +27,9 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
   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}{\color{blue}\underline{here}}. To get this node green, the proof (or another proof) needs to be upstreamed to mathlib.
 \end{proof}
 
-\begin{corollary}\label{WLOG_p_ge_5}\uses{p_not_three, WLOG_n_prime}\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\geq 5$.
+\begin{corollary}\label{WLOG_p_ge_5}\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\geq 5$.
 \end{corollary}
-\begin{proof}\leanok Follows from the previous two lemmas.\end{proof}
+\begin{proof}\uses{p_not_three, WLOG_n_prime}\leanok Follows from the previous two lemmas.\end{proof}
 
 \section{Frey packages}
 
@@ -39,10 +39,10 @@ \section{Frey packages}
 
 Our next reduction is as follows:
 
-\begin{lemma}\label{Frey_package_of_FLT_counterex}\lean{FLT.FreyPackage.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}\leanok
   If Fermat's Last Theorem is false, then there exists a Frey package.
 \end{lemma}
-\begin{proof} By Corollary \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 build a Frey package from this data.
+\begin{proof}\uses{Frey_package, WLOG_p_ge_5} By Corollary \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 build a Frey package from this data.
 
   If the greatest common divisor of $x,y,z$ is $d$ then $x^p+y^p=z^p$ implies $(x/d)^p+(y/d)^p=(z/d)^p$. Dividing through, we can thus assume that no prime divides all of $x,y,z$. Under this assumption we must have that $x,y,z$ are pairwise coprime, as if some prime divides two of the integers $x,y,z$ then by $x^p+y^p=z^p$ and unique factorization it must divide all three of them. In particular we may assume that not all of $x,y,z$ are even, and now reducing modulo~2 shows that precisely one of them must be even. 
 
@@ -75,16 +75,16 @@ \section{Galois representations and elliptic curves}
 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 \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
+\begin{theorem}[Mazur]\label{Mazur_on_Frey_curve}\lean{FLT.FreyCurve.Mazur_Frey}\tangled $\rho$ cannot be reducible.\end{theorem}
+\begin{proof}\uses{Frey_mod_p_Galois_representation} 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.
+\begin{theorem}[Wiles,Taylor--Wiles]\label{Wiles_on_Frey_curve}\lean{FLT.FreyCurve.Wiles_Frey}\leanok\tangled $\rho$ cannot be irreducible either.\end{theorem}
+\begin{proof}\uses{Frey_mod_p_Galois_representation} 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{no_Frey_package}\lean{FLT.Frey_package.false}\uses{Mazur_on_Frey_curve, Wiles_on_Frey_curve}\leanok There is no Frey package.\end{corollary}
@@ -94,5 +94,5 @@ \section{Galois representations and elliptic curves}
 
 \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.
+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}, and the corresponding Galois representation $\rho$ on the $p$-torsion of the Frey curve is neither reducible nor irreducible, a contradiction.
 \end{proof}