Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FLTPrelim_Modularity.lean

definition modulenamed in PROOF-PATH.mdnamed in route.md §4

Modularity of elliptic curves over ℚ via eigenform coefficients

The module fixes the project's notion of modularity in terms of q-expansion coefficients and point counts on a chosen integral equation. For f:\mathbb H\to\mathbb C, ModularFormClass.qCoeff f n is the n-th coefficient of Mathlib's q-expansion of f at width 1. CuspForm.IsNormalizedEigenform is a structure on a weight-2 cusp form f for \Gamma_0(N) whose fields are exactly the arithmetic of the coefficients: a_1=1; a_{mn}=a_ma_n for coprime m,n; a_{p^{r+2}}=a_pa_{p^{r+1}}-p\,a_{p^r} for all primes p\nmid N; and a_{p^{r+2}}=a_pa_{p^{r+1}} for primes p\mid N. No Hecke operator appears: being an eigenform is encoded purely by these recursions. On the curve side, for a Weierstrass curve over a finite ring the point type is finite (proved by injecting points into Option (R × R), the point at infinity going to none), the number of points of a Weierstrass curve over a commutative ring — Mathlib's affine point type, which includes the point at infinity — is given a name card, and traceOfFrobenius is \#F+1 minus that number. For W over \mathbb Z, reductionMod W p is the coefficientwise reduction to \mathbb Z/p and apOfModel W p its p+1-\#W(\mathbb F_p). Three predicates on integral equations follow: IsGoodPrimeFor W p is simply p\nmid\Delta(W); IsSemistableModel W says no prime divides both \Delta(W) and c_4(W); IsIntegralModelOf W E says some variable change over \mathbb Q carries E to the base change of W to \mathbb Q. Finally IsModularModelOfLevel W N asserts the existence of a weight-2 cusp form on \Gamma_0(N) satisfying the above recursions with a_p(f)=a_p(W) for every prime p with p\nmid\Delta(W) and p\nmid N; IsModularModel W adds N\ge 1; and IsModular E says some integral model of E is a modular model. Thus modularity is an equality of L-coefficients at good primes away from the level, not an assertion about a newform of the conductor, nor a Galois-representation isomorphism; semistability is a condition on the chosen equation rather than on E.

Relation to Mathlib

CuspForm, CongruenceSubgroup.Gamma0, q-expansions, WeierstrassCurve with its invariants c_4,\Delta, VariableChange and affine points are Mathlib's; the eigenform recursions, the counting function and trace of Frobenius, reduction modulo p, and the semistability, integral-model and modularity predicates are the project's own, together with a Finite instance for affine points over a finite ring.

Where it is used

These definitions give the statement of the modularity input to the proof: WeierstrassCurve.modularity_of_semistableModel derives IsModular from IsSemistableModel (with \Delta\ne0), and FreyPackage.frey_isModular applies it to the Frey curve attached to a counterexample to Fermat's Last Theorem. Nearly the whole tree below the modularity theorem is phrased in terms of these notions.

References

  1. A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  3. J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd edition, Graduate Texts in Mathematics 106, Springer, 2009

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_Modularity.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.NumberTheory.ModularForms.QExpansion ↗
import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups ↗
import Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange ↗
import Mathlib.Data.Finite.Card ↗
import Mathlib.Data.ZMod.Basic ↗

set_option autoImplicit false

noncomputable section

open UpperHalfPlane

universe u

namespace ModularFormClass

def qCoeff (f : ℍ → ℂ) (n : ℕ) : ℂ :=
  (qExpansion 1 f).coeff n

end ModularFormClass

namespace CuspForm

open ModularFormClass

structure IsNormalizedEigenform {N : ℕ} (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) :
    Prop where

  qCoeff_one : qCoeff f 1 = 1

  qCoeff_mul_of_coprime : ∀ m n : ℕ, m.Coprime n →
    qCoeff f (m * n) = qCoeff f m * qCoeff f n

  qCoeff_prime_pow_of_not_dvd : ∀ p r : ℕ, p.Prime → ¬ p ∣ N →
    qCoeff f (p ^ (r + 2)) = qCoeff f p * qCoeff f (p ^ (r + 1)) - p * qCoeff f (p ^ r)

  qCoeff_prime_pow_of_dvd : ∀ p r : ℕ, p.Prime → p ∣ N →
    qCoeff f (p ^ (r + 2)) = qCoeff f p * qCoeff f (p ^ (r + 1))

end CuspForm

namespace WeierstrassCurve

namespace Affine

variable {R : Type u} [CommRing R] {W' : Affine R}

private def Point.toOptionPair : W'.Point → Option (R × R)
  | .zero => none
  | .some x y _ => Option.some (x, y)

private lemma Point.toOptionPair_injective :
    Function.Injective (Point.toOptionPair (W' := W')) := by
  rintro (_ | ⟨x₁, y₁, h₁⟩) (_ | ⟨x₂, y₂, h₂⟩) h <;>
    simp only [Point.toOptionPair, Option.some.injEq, Prod.mk.injEq, reduceCtorEq] at h
  · rfl
  · obtain ⟨rfl, rfl⟩ := h; rfl

instance Point.instFinite [Finite R] : Finite W'.Point :=
  Finite.of_injective _ Point.toOptionPair_injective

end Affine

section Card

variable {F : Type u} [CommRing F] (W : WeierstrassCurve F)

def card : ℕ := Nat.card W.toAffine.Point

def traceOfFrobenius : ℤ := (Nat.card F : ℤ) + 1 - (W.card : ℤ)

end Card

def reductionMod (W : WeierstrassCurve ℤ) (p : ℕ) : WeierstrassCurve (ZMod p) :=
  W.map (Int.castRingHom (ZMod p))

def apOfModel (W : WeierstrassCurve ℤ) (p : ℕ) : ℤ :=
  (W.reductionMod p).traceOfFrobenius

def IsGoodPrimeFor (W : WeierstrassCurve ℤ) (p : ℕ) : Prop :=
  ¬ (p : ℤ) ∣ W.Δ

def IsSemistableModel (W : WeierstrassCurve ℤ) : Prop :=
  ∀ p : ℕ, p.Prime → (p : ℤ) ∣ W.Δ → ¬ (p : ℤ) ∣ W.c₄

def IsIntegralModelOf (W : WeierstrassCurve ℤ) (E : WeierstrassCurve ℚ) : Prop :=
  ∃ C : VariableChange ℚ, C • E = W.map (Int.castRingHom ℚ)

open CuspForm

def IsModularModelOfLevel (W : WeierstrassCurve ℤ) (N : ℕ) : Prop :=
  ∃ f : CuspForm (CongruenceSubgroup.Gamma0 N) 2, f.IsNormalizedEigenform ∧
    ∀ p : ℕ, p.Prime → W.IsGoodPrimeFor p → ¬ p ∣ N →
      ModularFormClass.qCoeff f p = (W.apOfModel p : ℂ)

def IsModularModel (W : WeierstrassCurve ℤ) : Prop :=
  ∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel N

def IsModular (E : WeierstrassCurve ℚ) : Prop :=
  ∃ W : WeierstrassCurve ℤ, W.IsIntegralModelOf E ∧ W.IsModularModel

end WeierstrassCurve

end

Statements phrased using this module (298)

… and 148 more statements (search for the module name to find them).