§5 Level lowering · FLT in Lean 4

5. Level lowering

theorem FreyPackage.level_lowering_to_two (P : FreyPackage) (hmod : P.freyCurve.IsModular) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) : ∃ f : CuspForm (CongruenceSubgroup.Gamma0 2) 2, f ≠ 0

Entry. FreyPackage.modularRepOfConductorLevel (P : FreyPackage) : ∃ N : ℕ, P.IsConductorLevel N ∧ P.ModularRepOfLevel N — the mod- $p$ representation of $E_{P}$ "arises from" a squarefree level $N$ all of whose prime factors divide $ab c$ (IsConductorLevel, Definitions/Def_FreyPackage_IsConductorLevel.lean), where ModularRepOfLevel P N (Definitions/Def_FLTPrelim_ModularRep.lean) means: a normalised weight-2 eigenform $f$ on $Γ_{0} (N)$ , an integral model $W$ of $E_{P}$ and a maximal ideal $m ∋ p$ of the algebraic integers with $a_{ℓ} (f) \equiv a_{ℓ} (W) (mod m)$ at good primes $ℓ ∤ N p$ — a congruence of traces, not an isomorphism of representations. This statement has no hypotheses: rather than consume the predicate IsModular, its proof re-runs the assembly of §4 for the integral Frey model, whose output is modularity of level exactly the product of the bad primes. (Consequently the hypothesis hmod of level_lowering_to_two is unused — its file disables the unused-variables linter: the two top-level steps share their modularity input rather than passing it through IsModular.)

Descent. FreyPackage.level_lowering_to_two_of_conductorLevel removes primes from $N$ one at a time by strong induction, keeping the invariant IsConductorLevel:

an odd prime $q \neq = p$ by FreyPackage.level_lowering_odd_prime_of_conductorLevel — Ribet's theorem in the form needed: if $E_{P} [p]$ is irreducible, unramified at $q$ (which it is, FreyPackage.freyGaloisRep_isUnramifiedAt, since $p ∣ v_{q} (Δ)$ ) and arises from a conductor-supported level $N$ with $q ∣ N$ , then it arises from a level $M ∣ N$ prime to $q$ . About 12,500 theorems lie below it, including essentially the whole CerednikDrinfeld namespace (2,376 theorems: Čerednik–Drinfeld uniformisation of Shimura curves, for Ribet's exchange between $J_{0} (N q)$ and the Jacobian of a Shimura curve) and the QuaternionAlgebra namespace (302); the curve-level core is WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf, and Eichler–Shimura (a mod- $m$ Galois representation attached to each weight-2 eigenform, FreyPackage.eigenformResidualAttachmentAtFamily) transports the congruence between levels and integral models;
the prime $p$ itself by FreyPackage.level_lowering_at_p_of_conductorLevel — the Mazur–Ribet step at $p$ , using that $E_{P} [p]$ is finite ("peu ramifié") at $p$ (FreyCurve.isPeuRamifieeAt_odd_of_integralForm) and the $a_{p}$ of a newform at a prime dividing the level (CuspForm.newformBadPrimeCoeff); about 6,100 theorems below it.

When only the prime 2 can divide the squarefree level, the level is 1 or 2; a normalised eigenform is nonzero, so ModularForm.S2_Gamma0_one_eq_zero and ModularForm.S2_Gamma0_2_eq_zero close the induction.

← §4 Modularity of semistable elliptic curves · §6 No cusp forms of weight 2 and level 2 →

How the theorems of this step depend on each other

Green cards are the landmarks named in this section; dashed white cards are landmarks of neighbouring steps they connect to. Premises above conclusions; an arrow may pass through unnamed intermediate theorems. Click a card for its page.

Theorems named in this section (10; statement as in the tree, numbers from the import graph)

Level lowering for the Frey curve down to $Γ_{0} (2)$ FreyPackage.level_lowering_to_two_of_conductorLevel

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_to_two_of_conductorLevel (P : FreyPackage) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) {N : ℕ} (hcond : P.IsConductorLevel N) (hmod : P.ModularRepOfLevel N) : ∃ f : CuspForm (CongruenceSubgroup.Gamma0 2) 2, f ≠ 0

12,980 theorems below · cites 5 · cited by 1 · depth 5 · proof 75 lines, 3 helpers

Ribet level lowering at an odd prime $q \neq = p$ FreyPackage.level_lowering_odd_prime_of_conductorLevel

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_odd_prime_of_conductorLevel (P : FreyPackage) {N q : ℕ} (hcond : P.IsConductorLevel N) (hq : q.Prime) (hq2 : q ≠ 2) (hqp : q ≠ P.p) (hqN : q ∣ N) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) (hmod : P.ModularRepOfLevel N) (hunr : P.GaloisRepUnramifiedAt q) : ∃ M : ℕ, M ∣ N ∧ ¬ q ∣ M ∧ P.ModularRepOfLevel M

12,496 theorems below · cites 10 · cited by 1 · depth 6 · proof 42 lines, 0 helpers

Frey $p$ -torsion is unramified outside ${2, p}$ FreyPackage.freyGaloisRep_isUnramifiedAt

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.freyGaloisRep_isUnramifiedAt (P : FreyPackage) {q : ℕ} (hq : q.Prime) (hq2 : q ≠ 2) (hqp : q ≠ P.p) : P.GaloisRepUnramifiedAt q

42 theorems below · cites 2 · cited by 2 · depth 6 · proof 158 lines, 11 helpers

Level lowering at an unramified prime exactly dividing the level WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf

set_option autoImplicit false
open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
theorem WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf
    (p : ℕ) [Fact p.Prime] (_hp2 : p ≠ 2) (W : WeierstrassCurve ℤ) (_hΔ : W.Δ ≠ 0)
    (_hW : W.IsSemistableModel)
    (hcard₁ : Nat.card (Submodule.torsionBy ℤ
      ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point p) = p ^ 2)
    (hker : GaloisFactorsThroughFiniteLevel
      (WeierstrassCurve.Affine.Point.galoisRepModuleEnd (K := AlgebraicClosure ℚ) ℚ
        (W.map (Int.castRingHom ℚ)) p))
    (_hirr : W.ModRepIsIrreducible p) (M q : ℕ) (hq : q.Prime) (hqp : q ≠ p)
    (hqM : q ∣ M) (hq2 : ¬ q ^ 2 ∣ M) (hM : Squarefree M)
    (hunr : ((W.map (Int.castRingHom ℚ)).residualGaloisRepOf p hcard₁ hker).IsUnramifiedAt q)
    (hres : W.IsResiduallyModularOfLevel p M) :
    W.IsResiduallyModularOfLevel p (M / q)

12,481 theorems below · cites 6 · cited by 3 · depth 7 · proof 103 lines, 2 helpers

Eichler–Shimura residual attachment at every level FreyPackage.eigenformResidualAttachmentAtFamily

theorem FreyPackage.eigenformResidualAttachmentAtFamily (P : FreyPackage) :
    ∀ M : ℕ, 0 < M → P.EigenformResidualAttachmentAt M

1,297 theorems below · cites 5 · cited by 2 · depth 7 · proof 16 lines, 0 helpers

Mazur–Ribet level lowering at $p$ for conductor levels FreyPackage.level_lowering_at_p_of_conductorLevel

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.level_lowering_at_p_of_conductorLevel (P : FreyPackage) {N : ℕ} (hcond : P.IsConductorLevel N) (hpN : P.p ∣ N) (hirr : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p) (hmod : P.ModularRepOfLevel N) : ∃ M : ℕ, M ∣ N ∧ ¬ P.p ∣ M ∧ P.ModularRepOfLevel M

6,090 theorems below · cites 4 · cited by 1 · depth 6 · proof 121 lines, 7 helpers

Frey curve is peu ramifiée at every odd prime FreyCurve.isPeuRamifieeAt_odd_of_integralForm

open FreyPackage
namespace FreyCurve
theorem isPeuRamifieeAt_odd_of_integralForm (P : FreyPackage) {q : ℕ} [Fact q.Prime]
    (hq2 : q ≠ 2) : P.freyCurve.IsPeuRamifieeAt P.p q

4 theorems below · cites 1 · cited by 2 · depth 7 · proof 6 lines, 0 helpers

Bad-prime coefficients of weight- $2$ newforms on $Γ_{0} (N)$ CuspForm.newformBadPrimeCoeff

set_option autoImplicit false
theorem CuspForm.newformBadPrimeCoeff (N : ℕ) :
    CuspForm.NewformBadPrimeCoeff N

68 theorems below · cites 2 · cited by 3 · depth 7 · proof 5 lines, 0 helpers

Weight-two cusp forms of level one vanish ModularForm.S2_Gamma0_one_eq_zero

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem ModularForm.S2_Gamma0_one_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 1) 2) : f = 0

0 theorems below · cites 0 · cited by 2 · depth 6 · proof 20 lines, 3 helpers

Vanishing of weight- $2$ cusp forms of level $2$ ModularForm.S2_Gamma0_2_eq_zero

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem ModularForm.S2_Gamma0_2_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0

0 theorems below · cites 0 · cited by 2 · depth 4 · proof 168 lines, 16 helpers

Definition modules named here

9,966 theorems of the tree are first reached through this step, in the sense that the first landmark met on a shortest citation path up to fermat_last_theorem is one named in this section. That is a reading aid, not a classification: the infrastructure below modularity and level lowering is largely shared.

← §4 Modularity of semistable elliptic curves · §6 No cusp forms of weight 2 and level 2 →