Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_LatticeHeckeFamily.lean

definition module

Commuting Hecke family on the integral lattice of cusp forms

Fix a level N \ge 1. The weight-two Hecke algebra \mathbb{T}_N = heckeAlgebra N 2 ∅ is the \mathbb{Z}-subalgebra of \operatorname{End}_{\mathbb{C}} S_2(\Gamma_0(N)) generated by the operators T_\ell for primes \ell \nmid N together with the operators U_q for primes q \mid N, no prime being excluded (the excluded set is \emptyset, so the side conditions \ell \notin S hold vacuously); it is commutative. The first definition, heckeAlgebra.atPrime N ℓ, assigns to a prime \ell a single element of \mathbb{T}_N by a case distinction on divisibility: it is U_\ell when \ell \mid N and T_\ell when \ell \nmid N. The two auxiliary lemmas heckeAlgebra.atPrime_of_dvd and heckeAlgebra.atPrime_of_not_dvd record exactly these two values.

The second definition, latticeHeckeFamily N, is a term of the structure ModularCurve.CommutingHeckeFamily on the integral lattice intLattice N 2, the \mathbb{Z}-submodule of S_2(\Gamma_0(N)) spanned by those cusp forms all of whose q-expansion coefficients are rational integers. That structure has two fields: a map from the primes to \operatorname{End}_{\mathbb{Z}} of the module, and the assertion that any two of its values commute. Here the endomorphism attached to \ell is the image of heckeAlgebra.atPrime N ℓ under the ring homomorphism latticeActionHom N ∅, that is, the restriction of the corresponding Hecke operator to the lattice (which the lattice is preserved by); commutativity of the images follows from commutativity of \mathbb{T}_N. The lemma latticeHeckeFamily_T states the defining equation for the member of the family at \ell.

Relation to Mathlib

Mathlib supplies the space CuspForm (CongruenceSubgroup.Gamma0 N) 2 and the q-expansion coefficients used to cut out the lattice; the integral lattice intLattice, the weight-two Hecke algebra heckeAlgebra as a \mathbb{Z}-subalgebra of endomorphisms, and the structure ModularCurve.CommutingHeckeFamily are the project's own notions.

Where it is used

A CommutingHeckeFamily determines, by evaluation of the polynomial algebra ModularCurve.HeckeAlg = \mathbb{Z}[T_\ell : \ell \text{ prime}] on its members, a module structure over that algebra; applied to latticeHeckeFamily N this makes the integral lattice of weight-two cusp forms of level N a HeckeAlg-module in which the generator indexed by \ell acts as T_\ell or U_\ell according to whether \ell divides N. This is the form in which the lattice enters the Hecke-module statements used for level lowering, where maximal ideals of residue characteristic p and their torsion submodules are the objects of study.

References

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

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CuspForm_HeckeLocal
import Definitions.Def_ModularCurve_SpecializationWitness

noncomputable section

namespace CuspForm

variable (N : ℕ) [NeZero N]

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

def latticeHeckeFamily : ModularCurve.CommutingHeckeFamily ↥(intLattice N 2) where
  T ℓ := latticeActionHom N ∅ (heckeAlgebra.atPrime N ℓ)
  comm q q' := (Commute.all (heckeAlgebra.atPrime N q) (heckeAlgebra.atPrime N q')).map (latticeActionHom N ∅)

theorem latticeHeckeFamily_T (ℓ : Nat.Primes) :
    (latticeHeckeFamily N).T ℓ = latticeActionHom N ∅ (heckeAlgebra.atPrime N ℓ) :=
  rfl

theorem heckeAlgebra.atPrime_of_dvd {ℓ : Nat.Primes} (h : (ℓ : ℕ) ∣ N) :
    heckeAlgebra.atPrime N ℓ = heckeAlgebra.U ℓ.2 h (Set.notMem_empty _) :=
  dif_pos h

theorem heckeAlgebra.atPrime_of_not_dvd {ℓ : Nat.Primes} (h : ¬ (ℓ : ℕ) ∣ N) :
    heckeAlgebra.atPrime N ℓ = heckeAlgebra.T ℓ.2 h (Set.notMem_empty _) :=
  dif_neg h

end CuspForm

end

Statements phrased using this module (7)