Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SupportTransfer.lean

definition module

Exit ideal of a Weierstrass model; support transfer

Throughout, N\ge 1 is a level, W a Weierstrass curve over \mathbb Z and p a natural number. The concrete coefficient ring is CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N}, the \mathbb Z-subalgebra of \mathrm{End}_{\mathbb C} S_2(\Gamma_0(N)) generated by the operators T_\ell for primes \ell\nmid N together with U_q for primes q\mid N outside the excluded set; since the excluded set is taken to be all divisors of N, no U_q occurs and the algebra is the anemic algebra \mathbb Z[T_\ell:\ell\nmid N].

For a prime \ell\nmid N, exitGen is the element T_\ell-a_\ell(W) of that algebra, where a_\ell(W) is W.apOfModel ℓ, namely \ell+1-\#\widetilde W(\mathbb F_\ell) for the coefficientwise reduction of W modulo \ell (points counted in the type of affine points together with the point at infinity), and the integer is embedded as a multiple of the identity. exitIdealGens is the set consisting of the image of p together with all T_\ell-a_\ell(W) for primes \ell with \ell\nmid N, \ell\neq p and \ell\nmid\Delta(W) (the predicate IsGoodPrimeFor), and exitIdeal is the ideal it spans; two short lemmas record that p and each such T_\ell-a_\ell(W) lie in this ideal.

Finally, for a finite set S of primes, an ideal \mathfrak m of the abstract Hecke algebra \mathbb T=\mathbb Z[X_\ell:\ell\ \text{prime}] and a \mathbb T-module J_0, SupportTransfer is the proposition asserting the single implication: if HasLowerLevelTorsion S 𝔪 J₀ holds — that is, if J_0 contains some y\neq 0 annihilated by every natural number whose image lies in \mathfrak m and by every element X_\ell-b\in\mathfrak m with \ell\notin S and b\in\mathbb Z — then \mathfrak m_0= exitIdeal N W p is a proper ideal. This is a named hypothesis, stated here and not proved; note that \mathfrak m is not assumed maximal and that it lies in the abstract polynomial algebra, whereas the exit ideal lies in the concrete algebra of operators on S_2(\Gamma_0(N)).

Relation to Mathlib

Mathlib supplies CuspForm, WeierstrassCurve and Ideal.span; the integral Hecke algebra acting on S_2(\Gamma_0(N)), the abstract Hecke algebra \mathbb T as a polynomial ring on the primes, and the exit ideal and support-transfer predicate are all the project's own.

Where it is used

The exit ideal is the ideal (p,\,T_\ell-a_\ell(W)) whose properness at level N produces, via a maximal ideal containing it and the Deligne–Serre argument, a weight-two level-N eigenform congruent to W. The support-transfer implication is the final clause of the Mazur-principle package: torsion at lower level in the abelian part of the Jacobian, detected by the Eichler–Shimura relations, is converted into properness of the exit ideal, which is how level lowering at an auxiliary prime is concluded for the Frey curve.

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. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §4.1

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_CuspForm_HeckeAlgebra
import Definitions.Def_ModularCurve_MazurPrincipleCore
import Definitions.Def_FLTPrelim_Modularity

set_option autoImplicit false

noncomputable section

namespace ModularCurve

section ExitIdeal

variable (N : ℕ) [NeZero N] (W : WeierstrassCurve ℤ) (p : ℕ)

def exitGen (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N) : CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N} :=
  CuspForm.heckeAlgebra.T (S := {n : ℕ | n ∣ N}) hℓ hℓN hℓN
    - ((W.apOfModel ℓ : ℤ) : CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N})

def exitIdealGens : Set (CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N}) :=
  insert ((p : ℕ) : CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N})
    {x | ∃ (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N),
      W.IsGoodPrimeFor ℓ ∧ ℓ ≠ p ∧ x = exitGen N W ℓ hℓ hℓN}

def exitIdeal : Ideal (CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N}) :=
  Ideal.span (exitIdealGens N W p)

theorem natCast_mem_exitIdeal : ((p : ℕ) : CuspForm.heckeAlgebra N 2 {n : ℕ | n ∣ N}) ∈ exitIdeal N W p :=
  Ideal.subset_span (Set.mem_insert _ _)

theorem exitGen_mem_exitIdeal (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N)
    (hgood : W.IsGoodPrimeFor ℓ) (hℓp : ℓ ≠ p) :
    exitGen N W ℓ hℓ hℓN ∈ exitIdeal N W p :=
  Ideal.subset_span (Set.mem_insert_of_mem _ ⟨ℓ, hℓ, hℓN, hgood, hℓp, rfl⟩)

end ExitIdeal

section SupportTransfer

variable (N : ℕ) [NeZero N] (W : WeierstrassCurve ℤ) (p : ℕ)
  (S : Finset Nat.Primes) (𝔪 : Ideal HeckeAlg)
  (J₀ : Type*) [AddCommGroup J₀] [Module HeckeAlg J₀]

def SupportTransfer : Prop :=
  HasLowerLevelTorsion S 𝔪 J₀ → exitIdeal N W p ≠ ⊤

end SupportTransfer

end ModularCurve

end

Statements phrased using this module (3)