Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FreyPackage_AtPNewLowering.lean

definition module

At- level lowering for -new witnesses: the predicate

The module defines a single proposition attached to a Frey package P (integers a,b,c, all nonzero, coprime with a\equiv 3 \pmod 4, b\equiv 0\pmod 2, and a prime p\ge 5 with a^p+b^p=c^p). FreyPackage.AtPNewLowering P says: for every N_0>0 with p\nmid N_0, if

(i) GaloisRepIsIrreducible holds for the Frey curve at p over \overline{\mathbb{Q}} — that is, the p-torsion submodule \mathrm{torsionBy}\,\mathbb{Z}\,E_P(\overline{\mathbb{Q}})\,p is nontrivial and every \mathbb{Z}/p-submodule stable under the action of \overline{\mathbb{Q}}\simeq_{\mathbb{Q}}\overline{\mathbb{Q}} is \bot or \top;

(ii) IsPeuRamifieeAt P.p P.p holds for P.freyCurve, which by definition means p \mid v_p(\Delta), the p-adic valuation of the discriminant of that particular Weierstrass presentation (a condition on the chosen model, not on a minimal model);

(iii) P.ModularRepOfLevelNewAt (N₀ * P.p) P.p holds: there exist a normalised eigenform g of weight 2 on \Gamma_0(N_0p), an integral Weierstrass model W of P.freyCurve (obtained by a rational variable change), and a maximal ideal \mathfrak{m} of the integral closure of \mathbb{Z} in \mathbb{C} containing p, such that for every prime \ell with \ell\nmid\Delta_W, \ell\nmid N_0p, \ell\ne p the q-coefficient a_\ell(g) is an algebraic integer congruent to a_\ell(W) modulo \mathfrak{m}, and moreover a_p(g)^2=1 (the project's IsNewAt condition, an exact equality of complex q-coefficients, rather than genuine p-newness);

then P.ModularRepOfLevel N₀ holds: the same congruence data exist at level N_0, for some normalised eigenform of weight 2 on \Gamma_0(N_0), some integral model of the Frey curve and some maximal ideal above p.

A classical DecidableEq instance on \overline{\mathbb{Q}} is provided locally, as the torsion-module constructions require it.

Relation to Mathlib

Mathlib has no notion of level lowering or of residual modularity; these are the project's own predicates, built on Mathlib's WeierstrassCurve, the group of affine points and Submodule.torsionBy, on CuspForm for CongruenceSubgroup.Gamma0 with its qExpansion coefficients, and on padicValRat for the peu-ramifiée condition.

Where it is used

This proposition is the form in which level lowering at the prime p itself enters the Frey–Serre–Ribet argument, complementing the lowering statements that remove auxiliary primes \ell\ne p: from a p-new witness of level N_0p congruent to the Frey curve it produces a witness of level N_0, which is what eventually forces a weight-2 eigenform of level too small to exist.

References

  1. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476
  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_FreyPackage_AtPNewLowering.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_FLTPrelim_FreyPackage
import Definitions.Def_FLTPrelim_GaloisRep
import Definitions.Def_FLTPrelim_ModularRep
import Definitions.Def_FreyPackage_LevelRaising
import Definitions.Def_WeierstrassCurve_PeuRamifiee

set_option autoImplicit false

noncomputable section

open WeierstrassCurve.Affine.Point

namespace FreyPackage

noncomputable local instance instDecEqQbarLedgerStageFour :
    DecidableEq (AlgebraicClosure ℚ) := Classical.decEq _

def AtPNewLowering (P : FreyPackage) : Prop :=
  ∀ N₀ : ℕ, 0 < N₀ → ¬ P.p ∣ N₀ →
    GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p →
    P.freyCurve.IsPeuRamifieeAt P.p P.p →
    P.ModularRepOfLevelNewAt (N₀ * P.p) P.p →
    P.ModularRepOfLevel N₀

end FreyPackage

end

Statements phrased using this module (1)