Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FLTPrelim_FreyPackage.lean

definition modulenamed in PROOF-PATH.mdnamed in route.md §2adapted from the Imperial College London FLT project: FLT/Basic/FreyPackage.lean

The Frey package and its Frey curve

A FreyPackage is a structure bundling a normalised putative counterexample to Fermat's Last Theorem: integers a, b, c, each assumed nonzero, a natural number p together with proofs that p is prime and 5 \le p, a proof of the equation a^p + b^p = c^p, and the normalisation hypotheses \gcd(a,b) = 1 (as the \mathbb{Z}-valued gcd of the GCD monoid \mathbb{Z}), a \equiv 3 \pmod 4 (stated as an equation in ZMod 4 on the image of a) and b \equiv 0 \pmod 2 (stated in ZMod 2). All of these are fields of the structure, so a term of type FreyPackage carries the equation and the congruences as data.

The accompanying lemmas record elementary consequences: p > 0, p \ne 0, p odd (from primality and p \ge 5); gcdab_eq_gcdac, a standalone lemma that for any integers with a^p + b^p = c^p and p > 0 one has \gcd(a,b) = \gcd(a,c); hence \gcd(a,c) = 1 and \gcd(b,c) = 1 for a package; abc \ne 0; and 2 \mid abc, deduced from 2 \mid b.

Two Weierstrass curves are then defined from a package P, by giving the five coefficients (a_1,a_2,a_3,a_4,a_6) directly: freyCurve over \mathbb{Q} and freyCurveInt over \mathbb{Z}, both with a_1 = 1, a_2 = (b^p - 1 - a^p)/4, a_3 = 0, a_4 = -a^p b^p/16, a_6 = 0. Thus the curve is y^2 + xy = x^3 + \frac{b^p - 1 - a^p}{4}x^2 - \frac{a^p b^p}{16}x, the standard integral model of y^2 = x(x - a^p)(x + b^p). Note that in freyCurveInt the two divisions are integer division in \mathbb{Z} (they are exact under the normalisation hypotheses, but the definition itself does not record this), whereas in freyCurve they are genuine division in \mathbb{Q}.

Relation to Mathlib

Mathlib has no notion of a Frey package; the structure is the project's own. The curves are ordinary terms of Mathlib's WeierstrassCurve over ℤ and over ℚ, with the coefficients supplied explicitly.

Where it is used

Every module of the main line of argument is phrased for a fixed FreyPackage: one is produced from an arbitrary counterexample to Fermat's Last Theorem with prime exponent p \ge 5, and the contradiction is obtained by studying the mod p representation on the Frey curve freyCurve — irreducibility, modularity, level lowering, and the absence of weight-2 cusp forms on \Gamma_0(2).

References

  1. G. Frey, Links between stable elliptic curves and certain Diophantine equations, Annales Universitatis Saraviensis, Series Mathematicae 1 (1986), 1–40
  2. J.-P. Serre, Sur les représentations modulaires de degré 2 de \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), Duke Mathematical Journal 54 (1987), 179–230
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_FLTPrelim_FreyPackage.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

/-
Copyright (c) 2024 Kevin Buzzard, Ruben Van de Velde, Pietro Monticone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Ported from the Imperial College London FLT formalization
(https://github.com/ImperialCollegeLondon/FLT, blueprint §2.5–2.6).
-/
import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass ↗
import Mathlib.Algebra.Field.ZMod ↗
import Mathlib.Algebra.GCDMonoid.Nat ↗
import Mathlib.Algebra.EuclideanDomain.Int ↗
import Mathlib.Data.Nat.Prime.Basic ↗
import Mathlib.RingTheory.Int.Basic ↗
import Mathlib.Tactic.ModCases ↗

set_option autoImplicit false

structure FreyPackage where

  a : ℤ

  b : ℤ

  c : ℤ
  ha0 : a ≠ 0
  hb0 : b ≠ 0
  hc0 : c ≠ 0

  p : ℕ
  pp : Nat.Prime p
  hp5 : 5 ≤ p

  hFLT : a ^ p + b ^ p = c ^ p

  hgcdab : gcd a b = 1

  ha4 : (a : ZMod 4) = 3

  hb2 : (b : ZMod 2) = 0

namespace FreyPackage

lemma hppos (P : FreyPackage) : 0 < P.p := lt_of_lt_of_le (by omega) P.hp5

lemma hp0 (P : FreyPackage) : P.p ≠ 0 := P.hppos.ne'

lemma hp_odd (P : FreyPackage) : Odd P.p :=
  P.pp.odd_of_ne_two (by have := P.hp5; omega)

lemma gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c ^ p) :
    gcd a b = gcd a c := by
  have foo : gcd a b ∣ gcd a c := by
    apply dvd_gcd (gcd_dvd_left a b)
    rw [← Int.pow_dvd_pow_iff hp.ne', ← h]
    apply dvd_add <;> rw [Int.pow_dvd_pow_iff hp.ne']
    · exact gcd_dvd_left a b
    · exact gcd_dvd_right a b
  have bar : gcd a c ∣ gcd a b := by
    apply dvd_gcd (gcd_dvd_left a c)
    have h2 : b ^ p = c ^ p - a ^ p := eq_sub_of_add_eq' h
    rw [← Int.pow_dvd_pow_iff hp.ne', h2]
    apply dvd_add
    · rw [Int.pow_dvd_pow_iff hp.ne']; exact gcd_dvd_right a c
    · rw [dvd_neg, Int.pow_dvd_pow_iff hp.ne']; exact gcd_dvd_left a c
  change _ ∣ (Int.gcd a c : ℤ) at foo
  apply Int.ofNat_dvd.1 at bar
  apply Int.ofNat_dvd.1 at foo
  exact congr_arg ((↑) : ℕ → ℤ) <| Nat.dvd_antisymm foo bar

lemma hgcdac (P : FreyPackage) : gcd P.a P.c = 1 := by
  rw [← gcdab_eq_gcdac P.hppos P.hFLT, P.hgcdab]

lemma hgcdbc (P : FreyPackage) : gcd P.b P.c = 1 := by
  rw [← gcdab_eq_gcdac P.hppos, gcd_comm, P.hgcdab]
  rw [add_comm]; exact P.hFLT

lemma habc0 (P : FreyPackage) : P.a * P.b * P.c ≠ 0 :=
  mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0

lemma two_dvd_abc (P : FreyPackage) : (2 : ℤ) ∣ P.a * P.b * P.c :=
  dvd_mul_of_dvd_left (dvd_mul_of_dvd_right
    ((ZMod.intCast_zmod_eq_zero_iff_dvd P.b 2).1 P.hb2) _) _

def freyCurveInt (P : FreyPackage) : WeierstrassCurve ℤ where
  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 freyCurve (P : FreyPackage) : WeierstrassCurve ℚ where
  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

end FreyPackage

Statements phrased using this module (97)