more tinkering with reductions.tex

blueprint/src/chapter/reductions.tex

@@ -5,7 +5,7 @@ \section{Overview}
 
 \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
 
-\begin{lemma}\label{WLOG_n_prime}\lean{FLT.FermatLastTheorem.of_odd_primes}\leanok
+\begin{lemma}\label{WLOG_n_prime}\lean{FermatLastTheorem.of_odd_primes}\leanok
   If there is a counterexample to Fermat's Last Theorem, then there is a counterexample $a^p+b^p=c^p$
   with $p$ an odd prime.
 \end{lemma}
@@ -20,7 +20,7 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
 
 Euler proved Fermat's Last Theorem for $p=3$; at the time of writing this is not in mathlib.
 
-\begin{lemma}\label{p_not_three}\lean{FLT.fermatLastTheoremThree}\leanok
+\begin{lemma}\label{p_not_three}\lean{fermatLastTheoremThree}\leanok
 %%\discussion{16}
 {\bf TODO} discussion.
   There are no nontrivial solutions in integers to $a^3+b^3=c^3$.
@@ -83,11 +83,11 @@ \section{Reduction to two big theorems.}
 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 a fair amount of work needs to be done to deduce the theorem from Mazur's result. We omit the reduction for now -- it is explained in Proposition~6 of~\cite{serreconj}. In brief, it uses 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). Mazur's theorem itself is of course way more difficult, and right now nobody is working on a formalisation as far as I know (it would be a substantial project in itself).
+\begin{proof}\tangled This follows from a profound result of Mazur \cite{mazur} 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]\label{Wiles_on_Frey_curve}\lean{FLT.FreyCurve.Wiles_Frey}\leanok $\rho$ cannot be irreducible either.\end{theorem}
-\begin{proof}\uses{Frey_mod_p_Galois_representation, frey_curve_hardly_ramified}\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{proof}\uses{Frey_mod_p_Galois_representation}\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}
 
 \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}