Merge branch 'main' of github.com:ImperialCollegeLondon/FLT

FLT/Basic/HardlyRamified.lean

@@ -0,0 +1,13 @@
+import Mathlib.Tactic
+
+/-
+Taylor: You could say that
+a representation
+
+r: G_Q -> GL_2(F_p)
+
+is *hardly ramified* if 1) det = cyclo, 2) unramified outside 2p, 3)
+r|_{G_p} comes from ffgs and r|_{G_2}^ss is unramified.
+
+Theorem: p-torsion in Frey curve is hardly ramified.
+-/

FLT/TateCurve.lean

@@ -4,6 +4,14 @@ Need Tate uniformisation from Silverman 2 Ch 5. Don't need surjectivity.
 May as well work over a general field complete wrt a nontrivial nonarch norm.
 
 Key result needed: Galois action on Qpbar-points of p-torsion of elliptic curve E
-is isomorphic to some explicit quotient of Qpbar^* by q(E)^ℤ.
+over Qp is isomorphic to some explicit quotient of Qpbar^* by q(E)^ℤ.
 
+One of the hardest parts of the argument is surjectivity; we don't need it so I propose
+we skip it. This enables the entire argument to be run over a field complete with respect
+to a nontrivial nonarchimedean real-valued norm.
+
+Key thing we want: injection from K^* / <q> into E(K) where K is a field complete wrt
+a nontriv nonarch norm, E is the Frey curve and q is chosen appropriately; proof that the injection is functorial in the sense that if K -> L
+is an injection of fields and the norm on L restricts to the norm on K then the obvious
+diagram commutes.
 -/

blueprint/src/chapter/frey.tex

@@ -0,0 +1,23 @@
+\chapter{The Frey Curve}
+
+\section{Overview}
+
+In the last chapter we explained how, given a counterexample to Fermat's Last Theorem we could construct a Frey curve, which is an elliptic curve with some interesting properties. Let $\rho:\GQ\to\GL_2(\Z/p\Z)$ be the representation on the $p$-torsion of this curve. In this chapter we discuss some basic properties of this representation, used both by Mazur to prove that $\rho$ cannot be reducible and by Wiles to prove that it can't be irreducible.
+
+\section{Hardly ramified representations}
+
+We make the following definition (this is not in the literature but it is a useful concept for us). We discuss the meaning of some of the concepts involved afterwards.
+
+\begin{stealthdefinition} Let $p\geq5$ be a prime. A representation $\rho: \GQ\to \GL_2(\Z/p\Z)$ is said to be \emph{hardly ramified} if it satisfies the following four axioms:
+  \begin{enumerate}
+  \item $\det(\rho)$ is the mod $p$ cyclotomic character;
+  \item $\rho$ is unramified outside $2p$;
+  \item The semisimplification of the restriction of $\rho$ to is unramified.
+  \item The restriction of $\rho$ to $\GQp$ comes from a finite flat group scheme;
+  \end{enumerate}
+\end{stealthdefinition}
+
+The theorem we want to discuss in this section is:
+
+\begin{theorem} If $\rho$ is the Galois representation on the $p$-torsion of the Frey curve coming from a Frey package, then $\rho$ is hardly ramified.
+\end{theorem}

blueprint/src/chapter/reductions.tex

@@ -48,7 +48,7 @@ \section{Frey packages}
 
   Next we show that we can find a counterexample with $y$ even. Indeed, if $x$ is even then we can switch $x$ and $y$, and if $z$ is even then we can replace $z$ by $-y$ and $y$ by $-z$ (using that $p$ is odd).
 
-  The last thing to ensure is that $x$ is 3 mod~4. We know that $x$ is odd, so it is either 1 or~3 mod~4. If $x$ is 3 mod~4 then we are home; if however $x$ is 1 mod~4 we replace $x,y,z$ by their negatives and this is the Frey package we seek.
+  The last thing to ensure is that $x$ is 3 mod~4. We know that $x$ is odd, so it is either~1 or~3 mod~4. If $x$ is 3 mod~4 then we are home; if however $x$ is 1 mod~4 we replace $x,y,z$ by their negatives and this is the Frey package we seek.
 \end{proof}
 
 \section{Galois representations and elliptic curves}
@@ -59,29 +59,34 @@ \section{Galois representations and elliptic curves}
 
 The group structure behaves well under change of field: If $K$ and $L$ are two fields of characteristic zero and $f:K\to L$ is a field homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive group homomorphism. This construction is functorial (it sends the identity to the identity, and compositions to compositions). Thus if $f$ is an isomorphism, then the induced map $E(K)\to E(L)$ is also an isomorphism, with the inverse morphism being the map $E(L)\to E(K)$ induced by $f^{-1}$. This construction thus gives us an action of the multiplicative group $\Aut(K)$ of automorphisms of the field $K$ on the additive abelian group $E(K)$. In particular, if $\Qbar$ denotes an algebraic closure of the rationals (for example, the algebraic numbers in $\bbC$) and if $\GQ$ denotes the group of field isomorphisms $\Qbar\to\Qbar$, then for any elliptic curve $E$ over $\Q$ we have an action of $\GQ$ on the additive abelian group $E(\Qbar)$.
 
-If $A$ is any additive abelian group, and if $p$ is a prime number, then the subgroup $A[p]$ of elements $a$ such that $pa=0$ is naturally a vector space over the field $\Z/p\Z$. If a group is acting on $A$ via additive group isomorphisms, then there will be an induced action of the group on $A[p]$, which thus inherits the stucture of a mod $p$ representation of $G$. Applying this to the above situation,
-if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to
-the curve $E$.
+We need a variant of this construction where we only consider the $p$-torsion of the curve. Recall that if $A$ is any additive abelian group, and if $p$ is a prime number, then the subgroup $A[p]$ of elements $a$ such that $pa=0$ is naturally a vector space over the field $\Z/p\Z$. If a group is acting on $A$ via additive group isomorphisms, then there will be an induced action of the group on $A[p]$, which thus inherits the stucture of a mod $p$ representation of $G$. Applying this to the above situation, we deduce that if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to the curve $E$.
 
-\begin{definition}[Frey]\label{Frey_curve}\lean{FLT.FreyCurve}\uses{Frey_package} Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellgouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p)$\end{definition}
+In the next section we explain which elliptic curve we will use.
 
-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$.
+\section{The Frey curve}
+
+\begin{stealthdefinition}[Frey]
+  Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellegouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p)$\end{stealthdefinition}
+
+\begin{theorem}\label{Frey_curve}\lean{FLT.FreyCurve}
+  The Frey curve is an elliptic curve over $\Q$.
+\end{theorem}
+\begin{proof}\uses{Frey_package} Indeed, the roots of the cubic $X(X-a^p)(X+b^p)$ are distinct because $a,b,c$ are nonzero and $a^p+b^p=c^p$.
+\end{proof}
 
 \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}
 
+Frey's observation is that this mod $p$ Galois representation has some very surprising properties. We will come back to this in the next chapter.
+
+\section{Reduction to two big theorems.}
+
 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 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?
+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}\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).
+\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).
 \end{proof}
-{\bf TODO two rferences above}
 
 \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.

blueprint/src/macro/common.tex

@@ -7,3 +7,7 @@
 \newcommand{\GQ}{\Gal(\Qbar/\Q)}
 \DeclareMathOperator{\Gal}{Gal}
 \DeclareMathOperator{\Aut}{Aut}
+\usepackage{amsthm}
+
+\newtheorem{stealthdefinition}{Definition}[chapter]
+