2. First Reductions Of The Problem
2.1. Goal
The goal of this chapter is to reduce FLT to a deep theorem of Mazur and a deep theorem of Wiles about a Galois representation.
2.2. Overview
The proof of Fermat's Last Theorem is by contradiction. We assume that we have
a counterexample a^n+b^n=c^n, and manipulate it until it satisfies the
axioms of a Frey package, a basic concept which we will explain below. From the
Frey package we build a Frey curve, an elliptic curve defined over \Q. We
then look at a certain representation of a Galois group coming from this
elliptic curve, and finally, using two very deep and independent theorems, one
due to Mazur and the other due to Wiles, we show that this representation is
both reducible and irreducible, the contradiction we seek.
2.3. Reduction To n >= 5 And Prime
-
FermatLastTheorem.of_odd_primes[complete]
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.
Lean code for Lemma2.3.1●1 theorem
Associated Lean declarations
-
FermatLastTheorem.of_odd_primes[complete]
-
FermatLastTheorem.of_odd_primes[complete]
-
theoremdefined in Mathlib/NumberTheory/FLT/Four.leancomplete
theorem FermatLastTheorem.of_odd_primes (hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem
theorem FermatLastTheorem.of_odd_primes (hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem
To prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.
This proof is already in mathlib, but the TeX blueprint spells it out for completeness.
Say a^n + b^n = c^n is a counterexample to Fermat's Last Theorem. Every
positive integer is either a power of 2 or has an odd prime factor. If
n = kp has an odd prime factor p, then
(a^k)^p + (b^k)^p = (c^k)^p, which is the counterexample we seek.
It remains to deal with the case where n is a power of 2, so let us assume
this. We have 3 \le n by assumption, so n = 4k is a multiple of 4, and
thus (a^k)^4 + (b^k)^4 = (c^k)^4, giving a counterexample to Fermat's Last
Theorem for n = 4. But Fermat's theorem for exponent 4, already in mathlib,
says that this is impossible.
Euler proved Fermat's Last Theorem for p = 3.
-
fermatLastTheoremThree[complete]
There are no solutions in positive integers to a^3+b^3=c^3.
Lean code for Lemma2.3.2●1 theorem
Associated Lean declarations
-
fermatLastTheoremThree[complete]
-
fermatLastTheoremThree[complete]
-
theoremdefined in Mathlib/NumberTheory/FLT/Three.leancomplete
theorem fermatLastTheoremThree : FermatLastTheoremFor 3
theorem fermatLastTheoremThree : FermatLastTheoremFor 3
Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then `a ^ 3 + b ^ 3 ≠ c ^ 3`.
The proof in mathlib was formalized by a team from the "Lean For the Curious
Mathematician" conference held in Luminy in March 2024 (its dependency graph
can be visualised here).
-
FermatLastTheorem.of_p_ge_5[complete]
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 \ge 5.
Lean code for Corollary2.3.3●1 theorem
Associated Lean declarations
-
FermatLastTheorem.of_p_ge_5[complete]
-
FermatLastTheorem.of_p_ge_5[complete]
-
theoremdefined in FLT/FreyCurve/FreyPackage.leancomplete
theorem FermatLastTheorem.of_p_ge_5 (H : ∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p) : FermatLastTheorem
theorem FermatLastTheorem.of_p_ge_5 (H : ∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p) : FermatLastTheorem
If Fermat's Last Theorem is true for primes `p ≥ 5`, then FLT is true.
Follows from the previous two lemmas.
2.4. Frey Packages
For convenience we make the following definition.
-
FreyPackage[complete]
A Frey package (a,b,c,p) is three nonzero pairwise-coprime integers a,
b, and c, with a \equiv 3 \pmod 4 and b \equiv 0 \pmod 2, together
with a prime p \ge 5, such that a^p+b^p=c^p.
Lean code for Definition2.4.1●1 definition
Associated Lean declarations
-
FreyPackage[complete]
-
FreyPackage[complete]
-
structuredefined in FLT/FreyCurve/FreyPackage.leancomplete
structure FreyPackage : Type
structure FreyPackage : Type
A *Frey Package* is a 4-tuple (a,b,c,p) of integers satisfying $a^p+b^p=c^p$ and some other inequalities and congruences. These facts guarantee that all of the all the results in section 4.1 of Serre's paper [serre] apply to the curve $Y^2=X(X-a^p)(X+b^p).$
Fields
a : ℤ
The integer `a` in the Frey package.
b : ℤ
The integer `b` in the Frey package.
c : ℤ
The integer `c` in the Frey package.
ha0 : self.a ≠ 0
hb0 : self.b ≠ 0
hc0 : self.c ≠ 0
p : ℕ
The prime number `p` in the Frey package.
pp : Nat.Prime self.p
hp5 : 5 ≤ self.p
hFLT : self.a ^ self.p + self.b ^ self.p = self.c ^ self.p
hgcdab : gcd self.a self.b = 1
ha4 : ↑self.a = 3
hb2 : ↑self.b = 0
Our next reduction is as follows.
If Fermat's Last Theorem is false for p prime and p \ge 5, then there
exists a Frey package.
Lean code for Lemma2.4.2●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/FreyCurve/FreyPackage.leancomplete
theorem FreyPackage.of_not_FermatLastTheorem_p_ge_5 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) {p : ℕ} (pp : Nat.Prime p) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FreyPackage
theorem FreyPackage.of_not_FermatLastTheorem_p_ge_5 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) {p : ℕ} (pp : Nat.Prime p) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FreyPackage
Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5, there exists a Frey package.
Suppose we have a counterexample a^p+b^p=c^p for the given p; we now build
a Frey package from this data.
If the greatest common divisor of a,b,c is d, then a^p+b^p=c^p implies
(a/d)^p+(b/d)^p=(c/d)^p. Dividing through, we can thus assume that no prime
divides all of a,b,c. Under this assumption we must have that a,b,c are
pairwise coprime, as if some prime divides two of the integers a,b,c then by
a^p+b^p=c^p and unique factorization it must divide all three of them. In
particular we may assume that not all of a,b,c are even, and now reducing
modulo 2 shows that precisely one of them must be even.
Next we show that we can find a counterexample with b even. If a is the
even one, then we can just switch a and b. If c is the even one, then we
can replace c by -b and b by -c, using that p is odd.
The last thing to ensure is that a is 3 mod 4. Because b is even, we
know that a is odd, so it is either 1 or 3 mod 4. If a is 3 mod 4
then we are home; if however a is 1 mod 4, we replace a,b,c by their
negatives, and this is the Frey package we seek.
2.5. 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 projectivization, is a so-called elliptic curve over
\Q.
If E : Y^2 = f(X) is an elliptic curve over \Q, and if K is any
characteristic zero field, and hence a \Q-algebra, 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" corresponding morally to x=y=\infty. It is an
extraordinary fact, and not at all obvious, that E(K) naturally has the
structure of an additive abelian group, with the point at infinity being the
zero element, the identity. Fortunately this fact is already in mathlib. This
additive group structure has the property that three distinct points P, Q,
R in K^2 which are in E(K) will sum to zero if and only if they are
collinear.
The group structure behaves well under change of field: if E is an elliptic
curve over \Q and if K\to L is a homomorphism of characteristic zero
fields, then the induced map E(K)\to E(L) is a group homomorphism. Thus if
f:K\to L is an isomorphism of characteristic zero fields, the induced map
E(K)\to E(L) is an isomorphism of groups, with the inverse isomorphism 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), and hence also on the n-torsion of this
group for any positive integer n. 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), and hence on its
n-torsion subgroup E(\Qbar)[n].
If furthermore n = p is prime, then E(\Qbar)[p] is naturally a vector space
over \Z/p\Z, and therefore it inherits the structure of a mod p
representation of \GQ. This is the mod p Galois representation attached to
the elliptic curve E, and it is well-known to be 2-dimensional. We call it
\rho_{E,p}.
In the next section we apply this theory to the elliptic curve coming from a counterexample to Fermat's Last Theorem.
2.6. The Frey Curve
Recall that a Frey package (a,b,c,p) is a prime p \ge 5 and nonzero
pairwise-coprime integers a, b, and c satisfying a^p+b^p=c^p and the
congruences a \equiv 3 \pmod 4 and b \equiv 0 \pmod 2. We have shown
above that if Fermat's Last Theorem is false, then a Frey package exists.
-
FreyPackage.freyCurve[complete]
Given a Frey package (a,b,c,p), the corresponding Frey curve is the elliptic
curve over \Q (considered by Frey and, before him, Hellegouarch) defined by the equation
Y^2 = X(X-a^p)(X+b^p).
Lean code for Definition2.6.1●1 definition
Associated Lean declarations
-
FreyPackage.freyCurve[complete]
-
FreyPackage.freyCurve[complete]
-
defdefined in FLT/FreyCurve/FreyPackage.leancomplete
def FreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚ
def FreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚ
The elliptic curve over `ℚ` 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. We put the curve into the form where the equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form. The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64.
Note that the roots of the cubic X(X-a^p)(X+b^p) are distinct because a,
b, and c are nonzero and a^p+b^p=c^p.
Given a Frey package (a,b,c,p) with corresponding Frey curve E, the mod
p Galois representation \rho_{E,p} attached to this package is the
2-dimensional representation of \GQ on E(\Qbar)[p] described above.
Frey's observation is that this representation has some very surprising
properties. We will make this remark more explicit in the next chapter. Here we
shall show how these properties can be used to finish the job.
2.7. Reduction To Two Big Theorems
Recall that a representation of a group G on a vector space W is said to be
irreducible if there are precisely two G-stable subspaces of W, namely 0
and W. The representation is said to be reducible otherwise.
Now say (a,b,c,p) is a Frey package. 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, and we say that \rho is the mod p representation associated to the
Frey package (a,b,c,p). Is \rho irreducible or not?
-
Mazur_Frey[sorry in proof]
If \rho is the mod p Galois representation associated to a Frey package
(a,b,c,p) then \rho is irreducible.
Lean code for Theorem2.7.1●1 theorem, incomplete
Associated Lean declarations
-
Mazur_Frey[sorry in proof]
-
Mazur_Frey[sorry in proof]
-
theoremdefined in FLT/FreyCurve/Contradiction.leancontains sorry
theorem Mazur_Frey (P : FreyPackage) : (P.freyCurve.galoisRep P.p ⋯).IsIrreducible
theorem Mazur_Frey (P : FreyPackage) : (P.freyCurve.galoisRep P.p ⋯).IsIrreducible
This follows from a profound and long result of Mazur
(Mazur, 1977) from 1977, namely the fact that the torsion
subgroup of an elliptic curve over \Q can have size at most 16. In fact
there is still a little more work which needs to be done to deduce the theorem
from Mazur's result. A pre-1990 reference for the full proof of this claim is
Proposition 6 in Section 4.1 of
(Serre, 1987).
Note that in the first (pre-2029) phase of the FLT project, we will not be
working on a formalization of this result, as it was known in the 1980s. We
will however be thinking a lot about the next result, which says the exact
opposite.
-
Wiles_Frey[complete]
If \rho is the mod p Galois representation associated to a Frey package
(a,b,c,p) then \rho is reducible.
Lean code for Theorem2.7.2●1 theorem
Associated Lean declarations
-
Wiles_Frey[complete]
-
Wiles_Frey[complete]
-
theoremdefined in FLT/FreyCurve/Contradiction.leancomplete
theorem Wiles_Frey (P : FreyPackage) : ¬(P.freyCurve.galoisRep P.p ⋯).IsIrreducible
theorem Wiles_Frey (P : FreyPackage) : ¬(P.freyCurve.galoisRep P.p ⋯).IsIrreducible
This follows from theorem Frey_curve_hardly_ramified, which shows that the
Frey representation is hardly ramified, together with theorem
hardly_ramified_reducible, which shows that any hardly ramified mod p
representation is reducible.
-
FreyPackage.false[complete]
There is no Frey package.
Lean code for Corollary2.7.3●1 theorem
Associated Lean declarations
-
FreyPackage.false[complete]
-
FreyPackage.false[complete]
-
theoremdefined in FLT/FreyCurve/Contradiction.leancomplete
theorem FreyPackage.false (P : FreyPackage) : False
theorem FreyPackage.false (P : FreyPackage) : False
There is no Frey package. This profound result is proved using work of Mazur and Wiles/Ribet to rule out all possibilities for the $p$-torsion in the corresponding Frey curve.
Follows immediately from the previous two theorems Theorem 2.7.1 and Theorem 2.7.2.
We deduce.
-
Wiles_Taylor_Wiles[complete]
Fermat's Last Theorem is true. In other words, there are no positive integers
a, b, and c and natural numbers n >= 3 such that a^n+b^n=c^n.
Lean code for Corollary2.7.4●1 theorem
Associated Lean declarations
-
Wiles_Taylor_Wiles[complete]
-
Wiles_Taylor_Wiles[complete]
-
theoremdefined in FLT/FreyCurve/Contradiction.leancomplete
theorem Wiles_Taylor_Wiles : FermatLastTheorem
theorem Wiles_Taylor_Wiles : FermatLastTheorem
Fermat's Last Theorem is true
Assume there is a there is a counterexample a^n+b^n=c^n. By Corollary
Corollary 2.3.3, we may assume that there is also a
counterexample a^p+b^p=c^p with p\geq 5 and prime. Then
Lemma 2.4.2 produces a Frey package,
contradicting Corollary 2.7.3.
Because we are, for now at least, assuming Mazur's theorem, we now turn our attention to a proof of theorem Theorem 2.7.2. We start on this proof in [??].