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

FLT/Basic/Reductions.lean

@@ -4,7 +4,7 @@ import Mathlib.Tactic
 import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
 import Mathlib.RepresentationTheory.Basic
 import Mathlib.RingTheory.SimpleModule
-import FLT.EllipticCurve.GaloisRepresentation
+import FLT.EllipticCurve.Torsion
 
 
 /-!
@@ -372,8 +372,6 @@ lemma of_not_FermatLastTheorem (h : ¬ FermatLastTheorem) : Nonempty (FreyPackag
   let ⟨a, b, c, ha, hb, hc, p, hpprime, hp, h⟩ := p_ge_5_counterexample_of_not_FermatLastTheorem h
   ⟨of_not_FermatLastTheorem_p_ge_5 ha hb hc hpprime hp h⟩
 
-end FreyPackage
-
 /-- The elliptic curve associated to a Frey package. The conditions imposed
 upon a Frey package guarantee that the running hypotheses in
 Section 4.1 of [Serre] all hold. -/
@@ -391,45 +389,38 @@ def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := {
     coe_Δ' := sorry -- check that the discriminant is correctly computed.
   }
 
-namespace FreyCurve
-
-abbrev Qbar := AlgebraicClosure ℚ
-
-open WeierstrassCurve
+end FreyPackage
 
--- this is wrong, it's the full group of points, not the p-torsion
-abbrev p_torsion (P : FreyPackage) : Type := ((FreyCurve P).toWeierstrassCurve ⟮Qbar⟯) -- need p-torsion
 
-variable (P : FreyPackage)
 
-instance : AddCommGroup (FreyCurve.p_torsion P) := sorry
-instance : Module (ZMod P.p) (FreyCurve.p_torsion P) := sorry -- definition above needs to be
-  -- fixed before this can be done
 
-def mod_p_Galois_representation (P : FreyPackage) :
-    Representation (ZMod P.p) (Qbar ≃ₗ[ℚ] Qbar) (FreyCurve.p_torsion P) := sorry
 
 /-!
 
-What can we say about this representation? It follows from a profound theorem
-of Mazur (and much other work) that this representation must be irreducible.
+Given an elliptic curve over `ℚ`, the p-torsion points defined over an algebraic
+closure of `ℚ` are a 2-dimensional Galois reprentation. What can we say about the Galois
+representation attached to the p-torsion of the Frey curve attached to a Frey package?
+
+It follows (after a little work!) from a profound theorem of Mazur that this representation
+must be irreducible.
 
 -/
 
+abbrev Qbar := AlgebraicClosure ℚ
+
+open WeierstrassCurve
 theorem Mazur_Frey (P : FreyPackage) :
-    IsSimpleModule (ZMod P.p) (mod_p_Galois_representation P).asModule := sorry
+    IsSimpleModule (ZMod P.p) (P.FreyCurve.mod_p_Galois_representation P.p Qbar).asModule := sorry
 
 /-!
 
-But it follows from a profound theorem of Ribet, and fact (proved by Wiles) that the Frey Curve
-is modular, that the representation cannot be irreducible.
+But it follows from a profound theorem of Ribet, and the even more profound theorem
+(proved by Wiles) that the Frey Curve is modular, that the representation cannot be irreducible.
 
 -/
 
 theorem Wiles_Frey (P : FreyPackage) :
-    ¬ IsSimpleModule (ZMod P.p) (mod_p_Galois_representation P).asModule := sorry
-
-end FreyCurve
+    ¬ IsSimpleModule (ZMod P.p) (P.FreyCurve.mod_p_Galois_representation P.p Qbar).asModule := sorry
 
 /-!
 
@@ -441,8 +432,8 @@ It follows that there is no Frey package.
 work of Mazur and Wiles/Ribet to rule out all possibilities for the
 $p$-torsion in the corresponding Frey curve. -/
 theorem FreyPackage.false (P : FreyPackage) : False := by
-  apply FreyCurve.Wiles_Frey P
-  exact FreyCurve.Mazur_Frey P
+  apply Wiles_Frey P
+  exact Mazur_Frey P
 
 -- Fermat's Last Theorem is true
 theorem Wiles_Taylor_Wiles : FermatLastTheorem := by

FLT/EllipticCurve/Torsion.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard
+-/
+import Mathlib.AlgebraicGeometry.EllipticCurve.Group
+import Mathlib.FieldTheory.IsSepClosed
+import Mathlib.RepresentationTheory.Basic
+
+/-!
+
+See
+https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/n-torsion.20or.20multiplication.20by.20n.20as.20an.20additive.20group.20hom/near/429096078
+
+The main theorems in this file are part of the PhD thesis work of David Angdinata, one of KB's
+PhD students. It would be great if anyone who is interested in working on these results
+could talk to David first. Note that he has already made substantial progress.
+
+-/
+
+universe u
+
+variable {K : Type u} [Field K] (E : EllipticCurve K)
+
+open WeierstrassCurve
+
+abbrev EllipticCurve.n_torsion (n : ℕ) : Type u := Submodule.torsionBy ℤ (E.toWeierstrassCurve ⟮K⟯) n
+
+--variable (n : ℕ) in
+--#synth AddCommGroup (E.n_torsion n)
+
+def ZMod.module (A : Type*) [AddCommGroup A] (n : ℕ) (hn : ∀ a : A, n • a = 0) :
+    Module (ZMod n) A :=
+  sorry
+
+-- not sure if this instance will cause more trouble than it's worth
+instance (n : ℕ) : Module (ZMod n) (E.n_torsion n) := sorry -- shouldn't be too hard
+
+-- This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata.
+-- Please do not work on it without talking to KB and David first.
+theorem EllipticCurve.n_torsion_finite {n : ℕ} (hn : 0 < n) : Finite (E.n_torsion n) := sorry
+
+-- This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata.
+-- Please do not work on it without talking to KB and David first.
+theorem EllipticCurve.n_torsion_card [IsSepClosed K] {n : ℕ} (hn : (n : K) ≠ 0) :
+    Nat.card (E.n_torsion n) = n^2 := sorry
+
+-- I only need this if n is prime but there's no harm thinking about it in general I guess.
+-- It follows from the previous theorem using pure group theory (possibly including the
+-- structure theorem for finite abelian groups)
+theorem EllipticCurve.n_torsion_dimension [IsSepClosed K] {n : ℕ} (hn : (n : K) ≠ 0) :
+    ∃ φ : E.n_torsion n ≃+ (ZMod n) × (ZMod n), True := sorry
+
+-- We need this -- ask David?
+example (L M : Type u) [Field L] [Field M] [Algebra K L] [Algebra K M] (f : L →ₐ[K] M) :
+    E.toWeierstrassCurve ⟮L⟯ →+ E.toWeierstrassCurve ⟮M⟯ := sorry
+
+-- Once we have it, plus the id and comp lemmas for it, we can get an action of Gal(K-bar/K) on E(K-bar)[n]
+def EllipticCurve.mod_p_Galois_representation (n : ℕ) (L : Type u) [Field L] [Algebra K L] :
+    Representation (ZMod n) (L ≃ₐ[K] L) (E.n_torsion n) := sorry

blueprint/src/chapter/introduction.tex → blueprint/src/chapter/ch01introduction.tex

@@ -4,6 +4,6 @@ \chapter{Introduction}
 
 Fermat's Last Theorem was explicitly raised by Fermat in 1637, and was proved by Wiles (with the proof completed in joint work with Taylor) in 1994. There are now several proofs but all of them go broadly in the same direction, using elliptic curves and modular forms.
 
-Explaining a proof of Fermat's Last Theorem to Lean is in some sense like explaining the proof to Diophantus; for example, the proof starts by observing that before we go any further it's convenient to first invent/discover zero and negative numbers, and one can point explicitly at places in Lean's source code \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Prelude.lean#L1049}{here} and \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Data/Int/Basic.lean#L45}{here} where these things happen. However we will adopt a more efficient approach: we will assume all of the theorems both in Lean and in its mathematics library \href{https://github.com/leanprover-community/mathlib4}{\tt mathlib}, and proceed from there.
+Explaining a proof of Fermat's Last Theorem to Lean is in some sense like explaining the proof to Diophantus; for example, the proof starts by observing that before we go any further it's convenient to first invent/discover zero and negative numbers, and one can point explicitly at places in Lean's source code \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Prelude.lean#L1049}{here} and \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Data/Int/Basic.lean#L45}{here} where these things happen. However we will adopt a more efficient approach: we will assume all of the theorems both in Lean and in its mathematics library \href{https://github.com/leanprover-community/mathlib4}{\tt mathlib}, and proceed from there. To give some idea of what this entails: {\tt mathlib} contains much of an undergraduate mathematics degree and parts of several relevant Masters level courses. Thus our task can be likened to the idea of teaching a graduate level course on Fermat's Last Theorem to a computer.
 
-The proof explained in these notes was constructed by Taylor, taking into account Buzzard's comments on what would be easy or hard to do in Lean. The proof uses refinements of the original Taylor-Wiles method by Diamond/Fujiwara, Khare/Wintenberger, Taylor and others. But it starts, as every known proof does, with some basic reductions and the introduction of a certain elliptic curve. We shall explain this next.
+The proof explained in these notes was constructed by Taylor, taking into account Buzzard's comments on what would be easy or hard to do in Lean. The proof uses refinements of the original Taylor-Wiles method by Diamond/Fujiwara, Khare/Wintenberger, Taylor and others. We shall explain more about the exact path we're taking in Chapter 4. But before we go into those technical details, we can enjoy some of the more basic arguments at the start of the proof. And the proof starts, as every known proof does, with some basic reductions and the introduction of a certain elliptic curve. We explain this in the next chapter.

blueprint/src/chapter/reductions.tex → blueprint/src/chapter/ch02reductions.tex

@@ -15,7 +15,7 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime}
   $(a^k)^p+(b^k)^p=(c^k)^p$ is the counterexample we seek. It remains to deal with the case where
   $n$ is a power of 2, so let's assume this. We have $3\leq n$ by assumption, so
   $n=4k$ must be a multiple of~4, and thus $(a^k)^4=(b^k)^4=(c^k)^4$, giving us a counterexample
-  to Fermat's Last Theorem for $n=4$. However an old result of Fermat himself (proved as {\tt fermatLastTheoremFour} in {\tt mathlib}) says that $x^4+y^4=z^4$ has no nontrivial solutions.
+  to Fermat's Last Theorem for $n=4$. However an old result of Fermat himself (proved as \href{https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/FLT/Four.html#fermatLastTheoremFour}{\tt fermatLastTheoremFour} in {\tt mathlib}) says that $x^4+y^4=z^4$ has no nontrivial solutions.
 \end{proof}
 
 Euler proved Fermat's Last Theorem for $p=3$; at the time of writing this is not in mathlib.
@@ -56,20 +56,20 @@ \section{Galois representations and elliptic curves}
 
 To continue, we need some of the theory of elliptic curves over $\Q$. So let $f(X)$ denote any monic cubic polynomial with rational coefficients and whose three complex roots are distinct, and let us consider the equation $E:Y^2=f(X)$, which defines a curve in the $(X,Y)$ plane. This curve (or strictly speaking its projectivisation) is a so-called elliptic curve (or an elliptic curve over $\Q$ if we want to keep track of the field where the coefficients of $f(X)$ lie). 
 
-If $E:Y^2=f(X)$ is as above, and if $K$ is any field of characteristic 0, then we write $E(K)$ for the set of solutions to $Y^2=f(X)$ with $X,Y\in K$, together with an additional ``point at infinity''. It is an extraordinary fact, and not at all obvious, that $E(K)$ naturally has the structure of an abelian group, and we shall use $+$ to denote the group law. This group structure has the property that three distinct points $P,Q,R\in E(K)$ in the $(X,Y)$ plane sum to zero if and only if they are collinear, and the point at infinity is the identity of the group.
+If $E:Y^2=f(X)$ is as above, and if $K$ is any field of characteristic 0, then we write $E(K)$ for the set of solutions to $Y^2=f(X)$ with $X,Y\in K$, together with an additional ``point at infinity''. It is an extraordinary fact, and not at all obvious, that $E(K)$ naturally has the structure of an abelian group, with the point at infinity being the identity element, and we shall use $+$ to denote the group law. This group structure has the property that three distinct points $P,Q,R\in E(K)$ in the $(X,Y)$ plane sum to zero if and only if they are collinear.
 
 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)$.
 
 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$.
 
-In the next section we explain which elliptic curve we will use.
+In the next section we apply this theory to an elliptic curve coming from a counterexample to Fermat's Last theorem.
 
 \section{The Frey curve}
 
 \begin{definition}[Frey]\label{Frey_curve}\lean{FLT.FreyCurve}
   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{definition}
 
-Note that  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$.
+Note that 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$.
 
 \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}
 
@@ -85,7 +85,7 @@ \section{Reduction to two big theorems.}
 \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{theorem}[Wiles,Taylor--Wiles, Ribet,\ldots]\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}\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,3 +98,5 @@ \section{Reduction to two big theorems.}
 \begin{proof}\leanok
 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}, contradicting Corollary~\ref{no_Frey_package}.
 \end{proof}
+
+The structure of the rest of this document is as follows. In Chapter 3 we develop some of the basic theory of elliptic curves and the Galois representations attached to their $p$-torsion subgroups. We then apply this theory to the Frey curve, deducing in particular how Mazur's result on torsion subgroups of elliptic curves implies Theorem~\ref{Mazur_on_Frey_curve}, the assertion that $\rho$ cannot be reducible. In Chapter 4 we give a high-level overview of our strategy to prove that $\rho$ cannot be irreducible, which diverges from the original approach taken by Wiles; one key difference is that we work with the $p$-torsion directly rather than switching to the 3-torsion. In Chapter 5 we give an overview of the theory of automorphic representations and their relationship to Galois representations.