From b63627cacb31a745c0f8c5f13784d1e322633a17 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 19 Mar 2024 16:51:03 +0000 Subject: [PATCH 1/2] remove \discussion for now in blueprint --- blueprint/src/chapter/reductions.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/blueprint/src/chapter/reductions.tex b/blueprint/src/chapter/reductions.tex index 8daf86d2..4b85017c 100644 --- a/blueprint/src/chapter/reductions.tex +++ b/blueprint/src/chapter/reductions.tex @@ -21,7 +21,8 @@ \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 -\discussion{16} +%%\discussion{16} +{\bf TODO} discussion. There are no nontrivial solutions in integers to $a^3+b^3=c^3$. \end{lemma} \begin{proof} From 6f7d99607acee3e478704748b5d59e92cad2cb95 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 19 Mar 2024 17:09:55 +0000 Subject: [PATCH 2/2] more tinkering with reductions.tex --- blueprint/src/chapter/reductions.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/blueprint/src/chapter/reductions.tex b/blueprint/src/chapter/reductions.tex index 4b85017c..1c4a52a9 100644 --- a/blueprint/src/chapter/reductions.tex +++ b/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}