Frey packages

A "Frey package" is a bundle of data consisting of nonzero pairwise coprime integers a, b, and c, and a prime p ≥ 5, such that a is 3 mod 4, b is even, and a^p+b^p=c^p.

The main result of this file is that if Fermat's Last Theorem is false, then there exists a Frey package.

The motivation behind this definition is that then all the results in Section 4.1 of Serre's paper [Serre] apply to the elliptic curve $Y^2=X(X-a^p)(X+b^p)$; this is the Frey curve associated to the Frey package.

Main definition

• FreyPackage : A Frey package is a triple (a,b,c) of nonzero, pairwise coprime integers and a prime p ≥ 5 such that a is 3 mod 4, b is even, and a^p+b^p=c^p.
• FreyPackage.freyCurve : The Frey curve associated to a Frey package.

Main theorem

• FreyPackage.of_not_FermatLastTheorem : A counterexample to FermatLastTheorem gives rise to a Frey Package.

The proof is an elementary arithmetic argument, assuming Fermat's result that FLT is true for n=4 and Euler's result that it's true for n=3.

We start by reducing the version of Fermat's Last Theorem for positive naturals to Lean's version FermatLastTheorem of the theorem.

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 corresponding Frey curve, the elliptic curve $Y^2=X(X-a^p)(X+b^p).$ In particular the $p$-torsion of this curve is a highly suspicious object. Serre could already prove in 1987 (using Mazur's theorem) that the $p$-torsion had to be an irreducible Galois representation; in 1990 Ribet proved that the $p$-torsion could not be irreducible, assuming modularity of the Frey curve. In 1993 Wiles showed that the Frey curve was modular, completing the proof.

• 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

  The integer a is nonzero.

• hb0 : self.b ≠ 0

  The integer b is nonzero.

• hc0 : self.c ≠ 0

  The integer c is nonzero.

• p : ℕ

  The prime number p in the Frey package.

• pp : Nat.Prime self.p

  The natural number p is prime.

• hp5 : 5 ≤ self.p

  The prime p is at least 5.

• hFLT : self.a ^ self.p + self.b ^ self.p = self.c ^ self.p

  The Fermat equation a ^ p + b ^ p = c ^ p holds.

• hgcdab : gcd self.a self.b = 1

  The integers a and b are coprime. Together with hFLT this is equivalent to a, b and c being pairwise coprime.

• ha4 : ↑self.a = 3

  The integer a is congruent to 3 modulo 4.

• hb2 : ↑self.b = 0

  The integer b is even, i.e. congruent to 0 modulo 2.

theorem FreyPackage.hppos (P : FreyPackage) : 0 < P.p

theorem FreyPackage.hp0 (P : FreyPackage) : P.p ≠ 0

theorem FreyPackage.hp_odd (P : FreyPackage) : Odd P.p

theorem FreyPackage.gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c ^ p) : gcd a b = gcd a c

theorem FreyPackage.hgcdac (P : FreyPackage) : gcd P.a P.c = 1

theorem FreyPackage.hgcdbc (P : FreyPackage) : gcd P.b P.c = 1

theorem FreyPackage.of_not_FermatLastTheoremFor_p_ge_5 {p : ℕ} (pp : Nat.Prime p) (hp5 : 5 ≤ p) (H : ¬FermatLastTheoremFor p) : Nonempty FreyPackage

Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package.

theorem FreyPackage.fermatLastTheoremFor_p_ge_5 (h : IsEmpty FreyPackage) (p : ℕ) : p ≥ 5 → Nat.Prime p → FermatLastTheoremFor p

If there is no Frey package, then Fermat's Last Theorem is true for all primes p≥5.