Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FreyPackage_LevelRaising.lean

definition module

Level raising for Frey packages: witnesses new at a prime

Four items are defined. First, for a weight-2 cusp form g on \Gamma_0(M) and a natural number q, CuspForm.IsNewAt asserts the single equation a_q(g)^2 = 1 on the q-expansion coefficient a_q(g) (the q-th coefficient of the expansion of g with respect to the parameter of width 1); this is a numerical condition on one coefficient, not the span-theoretic definition of newness, and no relation between q and M is required.

Second, FreyPackage.IsCongruentWitness P N f W π”ͺ packages the data used throughout to say that the mod-p representation attached to the Frey curve of a Frey package P=(a,b,c,p) comes from level N: f is a normalized Hecke eigenform of weight 2 on \Gamma_0(N) in the project's coefficient-wise sense (a_1=1, multiplicativity at coprime indices, and the two prime-power recursions according as p \mid N or not); W is an integral Weierstrass model of P.freyCurve, i.e. some variable change over \mathbb{Q} carries the Frey curve to the base change of W; \mathfrak{m} is a maximal ideal of the ring of algebraic integers in \mathbb{C} containing p; and for every prime \ell with \ell \nmid \Delta_W, \ell \nmid N, \ell \neq p, the coefficient a_\ell(f) is an algebraic integer congruent modulo \mathfrak{m} to \#\mathbb{F}_\ell + 1 - \#W_{/\mathbb{F}_\ell}. This is literally the existential body of ModularRepOfLevel, now named. Third, ModularRepOfLevelNewAt P M q asserts the existence of such a witness at level M whose form is new at q in the above sense.

Finally, FreyPackage.LevelRaising P N q' is the implication: for all f, W, \mathfrak{m}, if N>0, q' is prime with q' \nmid N and q' \neq p, the p-torsion of the Frey curve over \overline{\mathbb{Q}} is irreducible as a Galois module in the project's sense (nontrivial, with no Galois-stable \mathbb{Z}/p-submodules other than \bot and \top), (f,W,\mathfrak{m}) is a congruent witness at level N, and a_{q'}(f)^2 \equiv (q'+1)^2 \pmod{\mathfrak{m}}, then ModularRepOfLevelNewAt P (N*q') q' holds.

Relation to Mathlib

Mathlib supplies CuspForm, the groups \Gamma_0(N) and the q-expansion machinery, together with Weierstrass curves and the integral closure of \mathbb{Z} in \mathbb{C}; newness, congruent witnesses and the level-raising property are the project's own notions, as are the normalized-eigenform and integral-model predicates they use. A local DecidableEq (AlgebraicClosure β„š) instance is obtained from classical choice, as required by the project's Galois-module irreducibility predicate.

Where it is used

LevelRaising is the hypothesis form of Ribet's level-raising theorem as it is needed for the Frey curve: it allows a prime q' satisfying the congruence a_{q'}^2 \equiv (q'+1)^2 to be inserted into the level, producing a witness new at q'. It is used alongside ModularRepOfLevel in the level-lowering step which contradicts the existence of a Frey package.

References

  1. K. A. Ribet, Raising the levels of modular representations, in: SΓ©minaire de ThΓ©orie des Nombres, Paris 1987–88, Progress in Mathematics 81, BirkhΓ€user, 1990, 259–271
  2. K. A. Ribet, Congruence relations between modular forms, in: Proceedings of the International Congress of Mathematicians, Warsaw 1983, 503–514
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Theorem 3.35

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

Imports

Imported by

Declarations

Source

import Mathlib.NumberTheory.NumberField.Basic β†—
import Mathlib.RingTheory.Ideal.Basic β†—
import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass β†—
import Definitions.Def_FLTPrelim_ModularRep

set_option autoImplicit false

open WeierstrassCurve WeierstrassCurve.Affine.Point

open scoped CongruenceSubgroup

namespace CuspForm

def IsNewAt {M : β„•} (g : CuspForm (CongruenceSubgroup.Gamma0 M) 2) (q : β„•) : Prop :=
  ModularFormClass.qCoeff g q ^ 2 = 1

end CuspForm

namespace FreyPackage

noncomputable local instance instDecEqQbarLevelRaising :
    DecidableEq (AlgebraicClosure β„š) := Classical.decEq _

def IsCongruentWitness (P : FreyPackage) (N : β„•)
    (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) (W : WeierstrassCurve β„€)
    (π”ͺ : Ideal (integralClosure β„€ β„‚)) : Prop :=
  f.IsNormalizedEigenform ∧ W.IsIntegralModelOf P.freyCurve ∧
    π”ͺ.IsMaximal ∧ (P.p : integralClosure β„€ β„‚) ∈ π”ͺ ∧
    βˆ€ β„“ : β„•, β„“.Prime β†’ W.IsGoodPrimeFor β„“ β†’ Β¬ β„“ ∣ N β†’ β„“ β‰  P.p β†’
      βˆƒ a : integralClosure β„€ β„‚, (a : β„‚) = ModularFormClass.qCoeff f β„“ ∧
        a - ((W.apOfModel β„“ : β„€) : integralClosure β„€ β„‚) ∈ π”ͺ

def ModularRepOfLevelNewAt (P : FreyPackage) (M q : β„•) : Prop :=
  βˆƒ (g : CuspForm (CongruenceSubgroup.Gamma0 M) 2) (W : WeierstrassCurve β„€)
    (π”ͺ : Ideal (integralClosure β„€ β„‚)), P.IsCongruentWitness M g W π”ͺ ∧ g.IsNewAt q

def LevelRaising (P : FreyPackage) (N q' : β„•) : Prop :=
  βˆ€ (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) (W : WeierstrassCurve β„€)
    (π”ͺ : Ideal (integralClosure β„€ β„‚)),
    0 < N β†’ q'.Prime β†’ Β¬ q' ∣ N β†’ q' β‰  P.p β†’
    GaloisRepIsIrreducible (K := AlgebraicClosure β„š) β„š P.freyCurve P.p β†’
    P.IsCongruentWitness N f W π”ͺ β†’
    (βˆƒ a : integralClosure β„€ β„‚, (a : β„‚) = ModularFormClass.qCoeff f q' ∧
      a ^ 2 - ((q' : integralClosure β„€ β„‚) + 1) ^ 2 ∈ π”ͺ) β†’
    P.ModularRepOfLevelNewAt (N * q') q'

end FreyPackage

Statements phrased using this module (6)