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.

theorem PNat.pow_add_pow_ne_pow_of_FermatLastTheorem : FermatLastTheorem → ∀ (a b c : ℕ+), ∀ n > 2, a ^ n + b ^ n ≠ c ^ n

Fermat's Last Theorem as stated in mathlib (a statement FermatLastTheorem about naturals) implies Fermat's Last Theorem stated in terms of positive integers.

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.

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).$

• 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

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_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.

theorem FreyPackage.of_not_FermatLastTheorem (h : ¬FermatLastTheorem) : Nonempty FreyPackage

If Fermat's Last Theorem is false, then there exists a Frey Package.

def FreyPackage.freyCurveInt (P : FreyPackage) : WeierstrassCurve ℤ

The Weierstrass 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.

Equations

• P.freyCurveInt = { a₁ := 1, a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4, a₃ := 0, a₄ := -P.a ^ P.p * P.b ^ P.p / 16, a₆ := 0 }

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.

Equations

• P.freyCurve = { a₁ := 1, a₂ := (↑P.b ^ P.p - 1 - ↑P.a ^ P.p) / 4, a₃ := 0, a₄ := -↑P.a ^ P.p * ↑P.b ^ P.p / 16, a₆ := 0 }

theorem FreyCurve.map (P : FreyPackage) : P.freyCurveInt.map (algebraMap ℤ ℚ) = P.freyCurve

theorem FreyCurve.Δ (P : FreyPackage) : P.freyCurve.Δ = (↑P.a * ↑P.b * ↑P.c) ^ (2 * P.p) / 2 ^ 8

instance FreyCurve.instIsEllipticRatFreyCurve (P : FreyPackage) : P.freyCurve.IsElliptic

theorem FreyCurve.b₂ (P : FreyPackage) : P.freyCurve.b₂ = ↑P.b ^ P.p - ↑P.a ^ P.p

theorem FreyCurve.b₄ (P : FreyPackage) : P.freyCurve.b₄ = -(↑P.a * ↑P.b) ^ P.p / 8

theorem FreyCurve.c₄ (P : FreyPackage) : P.freyCurve.c₄ = (↑P.a ^ P.p) ^ 2 + ↑P.a ^ P.p * ↑P.b ^ P.p + (↑P.b ^ P.p) ^ 2

theorem FreyCurve.c₄' (P : FreyPackage) : P.freyCurve.c₄ = ↑P.c ^ (2 * P.p) - (↑P.a * ↑P.b) ^ P.p

theorem FreyCurve.Δ'inv (P : FreyPackage) : ↑P.freyCurve.Δ'⁻¹ = 2 ^ 8 / (↑P.a * ↑P.b * ↑P.c) ^ (2 * P.p)

theorem FreyCurve.j (P : FreyPackage) : P.freyCurve.j = 2 ^ 8 * (↑P.c ^ (2 * P.p) - (↑P.a * ↑P.b) ^ P.p) ^ 3 / (↑P.a * ↑P.b * ↑P.c) ^ (2 * P.p)

theorem FreyCurve.j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime : Nat.Prime q) (hqbad : ↑q ∣ P.a * P.b * P.c) (hqodd : 2 < q) : ↑P.p ∣ padicValRat q P.freyCurve.j

The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction.