Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_HeckeEvalForms.lean

definition module

Evaluating the abstract Hecke algebra on cusp forms

Fix a level N \ge 1 and a weight k \in \mathbb{Z}. The abstract Hecke algebra ModularCurve.HeckeAlg is the polynomial ring \mathbb{Z}[X_\ell] over the type of primes, with X_\ell = ModularCurve.heckeGen \ell; the analytic side is CuspForm.heckeAlgebra N k ∅, the \mathbb{Z}-subalgebra of \operatorname{End}_{\mathbb{C}} S_k(\Gamma_0(N)) generated by the operators heckeTLin for primes \ell \nmid N together with heckeULin for primes q \mid N, no prime being excluded since the exceptional set is empty. Two declarations are made. First, heckeFormsGen N k ℓ assigns to each prime \ell an element of that subalgebra: it is the bundled element heckeAlgebra.U attached to heckeULin when \ell \mid N, and the bundled element heckeAlgebra.T attached to heckeTLin when \ell \nmid N; the two accompanying lemmas record these two branches. Second, heckeEvalForms N k is the ring homomorphism \mathbb{Z}[X_\ell] \to heckeAlgebra N k ∅ obtained as the \mathbb{Z}-algebra evaluation map at the family heckeFormsGen N k, viewed as a map of rings. Its characteristic properties are recorded: the generator X_\ell goes to heckeFormsGen N k ℓ, hence to U_q for q \mid N and to T_\ell for \ell \nmid N; and a constant polynomial C(a), a \in \mathbb{Z}, goes to the image of a under the structure map \mathbb{Z} \to heckeAlgebra N k ∅. Because the assignment is defined for every prime, the target must be the Hecke algebra with empty exceptional set.

Relation to Mathlib

The abstract Hecke algebra is Mathlib's MvPolynomial ring over \mathbb{Z} and the evaluation map is Mathlib's MvPolynomial.aeval; the target, an algebra of Hecke operators on S_k(\Gamma_0(N)) built from slash actions, is the project's own construction.

Where it is used

The homomorphism provides the dictionary between the abstract Hecke algebra, in whose terms eigensystems, Eisenstein ideals and the local conditions at Frobenius are phrased, and operators genuinely acting on cusp forms of level \Gamma_0(N), as needed on the Hecke side of the Eichler–Shimura comparison and in the passage between eigenforms and Galois representations.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, Chapter 5
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, Chapter 3

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CuspForm_HeckeAlgebra
import Definitions.Def_HeckeGalois_EichlerShimura

set_option autoImplicit false

noncomputable section

namespace CuspForm

variable (N : ℕ) [NeZero N] (k : ℤ)

def heckeFormsGen (ℓ : Nat.Primes) : heckeAlgebra N k ∅ :=
  if h : (ℓ : ℕ) ∣ N then heckeAlgebra.U ℓ.2 h (Set.notMem_empty _)
  else heckeAlgebra.T ℓ.2 h (Set.notMem_empty _)

variable {N k} in
theorem heckeFormsGen_of_dvd {q : Nat.Primes} (h : (q : ℕ) ∣ N) :
    heckeFormsGen N k q = heckeAlgebra.U q.2 h (Set.notMem_empty _) :=
  dif_pos h

variable {N k} in
theorem heckeFormsGen_of_not_dvd {ℓ : Nat.Primes} (h : ¬ (ℓ : ℕ) ∣ N) :
    heckeFormsGen N k ℓ = heckeAlgebra.T ℓ.2 h (Set.notMem_empty _) :=
  dif_neg h

def heckeEvalForms : ModularCurve.HeckeAlg →+* heckeAlgebra N k ∅ :=
  (MvPolynomial.aeval (heckeFormsGen N k)).toRingHom

theorem heckeEvalForms_heckeGen (ℓ : Nat.Primes) :
    heckeEvalForms N k (ModularCurve.heckeGen ℓ) = heckeFormsGen N k ℓ :=
  MvPolynomial.aeval_X _ ℓ

variable {N k} in
theorem heckeEvalForms_heckeGen_of_dvd {q : Nat.Primes} (h : (q : ℕ) ∣ N) :
    heckeEvalForms N k (ModularCurve.heckeGen q) = heckeAlgebra.U q.2 h (Set.notMem_empty _) := by
  rw [heckeEvalForms_heckeGen, heckeFormsGen_of_dvd h]

variable {N k} in
theorem heckeEvalForms_heckeGen_of_not_dvd {ℓ : Nat.Primes} (h : ¬ (ℓ : ℕ) ∣ N) :
    heckeEvalForms N k (ModularCurve.heckeGen ℓ) = heckeAlgebra.T ℓ.2 h (Set.notMem_empty _) := by
  rw [heckeEvalForms_heckeGen, heckeFormsGen_of_not_dvd h]

theorem heckeEvalForms_C (a : ℤ) :
    heckeEvalForms N k (MvPolynomial.C a) = algebraMap ℤ (heckeAlgebra N k ∅) a :=
  MvPolynomial.aeval_C _ a

end CuspForm

end

Statements phrased using this module (28)