Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeProj.lean

definition module

Projection of the abstract Hecke algebra to level

Fix a level N \neq 0. The abstract Hecke algebra of the project is the polynomial ring \mathbb{T} = HeckeAlg = \mathbb{Z}[X_\ell : \ell \text{ prime}] on one variable heckeGen ℓ = X_\ell for each prime, while the concrete weight-two Hecke algebra at level N is CuspForm.heckeAlgebra N 2 ∅, the \mathbb{Z}-subalgebra of \operatorname{End}_{\mathbb{C}} S_2(\Gamma_0(N)) generated by the operators CuspForm.heckeTLin attached to primes \ell \nmid N and CuspForm.heckeULin attached to primes q \mid N (each of these being the endomorphism of cusp forms induced by the corresponding sum of slash operators, f \mapsto \sum_{j<p} f\mid_k \begin{pmatrix}1&j\\0&p\end{pmatrix}, with the extra term f\mid_k \begin{pmatrix}p&0\\0&1\end{pmatrix} in the T case); the empty excluded set S = \varnothing means no prime is omitted from the generating family.

The element heckeProjGen N ℓ of this subalgebra is defined by a case distinction on divisibility: it is CuspForm.heckeAlgebra.U at \ell when \ell \mid N, and CuspForm.heckeAlgebra.T at \ell when \ell \nmid N. Then heckeProj N is the ring homomorphism \mathbb{T} \to CuspForm.heckeAlgebra N 2 ∅ underlying the \mathbb{Z}-algebra evaluation map that sends X_\ell to heckeProjGen N ℓ; this makes sense because the subalgebra is commutative.

The accompanying lemmas record the interface: heckeProj_heckeGen_of_not_dvd and heckeProj_heckeGen_of_dvd evaluate the map on a variable X_\ell as T_\ell respectively U_\ell, with the divisibility hypothesis supplied by the caller; heckeProj_C identifies the image of a constant c \in \mathbb{Z} with c under the structure map of the subalgebra; and ringHom_ext_heckeProj states that two ring homomorphisms f, g from CuspForm.heckeAlgebra N 2 ∅ to a ring R which agree on every element heckeProjGen N ℓ have equal composites f \circ heckeProj N = g \circ heckeProj N. Note that this is an extensionality principle for the composites only; it yields f = g exactly when heckeProj N is known to be surjective.

Relation to Mathlib

Mathlib supplies CuspForm, CongruenceSubgroup.Gamma0, the slash action and MvPolynomial, but no Hecke operators on spaces of modular forms and no Hecke algebra; the polynomial model HeckeAlg of the abstract Hecke algebra, the operators CuspForm.heckeTLin, CuspForm.heckeULin, the subalgebra CuspForm.heckeAlgebra and the projection defined here are all proper to this development.

Where it is used

The abstract Hecke algebra \mathbb{T} is the ring through which Hecke eigensystems, the Eisenstein ideal and the Galois-theoretic clauses of the Eichler–Shimura package are formulated, while CuspForm.heckeAlgebra N 2 ∅ acts on actual weight-two cusp forms of level \Gamma_0(N). The homomorphism defined here is what transports statements about ideals of \mathbb{T}, in particular about the Eisenstein ideal and about maximal ideals cutting out mod-p eigensystems, into assertions about the operators T_\ell and U_q acting on S_2(\Gamma_0(N)).

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, Chapter 5

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_HeckeGalois_EichlerShimura
import Definitions.Def_CuspForm_HeckeAlgebra

noncomputable section

namespace ModularCurve

variable (N : ℕ) [NeZero N]

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

def heckeProj : HeckeAlg →+* CuspForm.heckeAlgebra N 2 ∅ :=
  (MvPolynomial.aeval (R := ℤ) (heckeProjGen N)).toRingHom

variable {N}

theorem heckeProj_heckeGen_of_not_dvd (ℓ : Nat.Primes) (h : ¬ (ℓ : ℕ) ∣ N) :
    heckeProj N (heckeGen ℓ) = CuspForm.heckeAlgebra.T ℓ.2 h (Set.notMem_empty _) := by
  simp [heckeProj, heckeGen, heckeProjGen, h]

theorem heckeProj_heckeGen_of_dvd (ℓ : Nat.Primes) (h : (ℓ : ℕ) ∣ N) :
    heckeProj N (heckeGen ℓ) = CuspForm.heckeAlgebra.U ℓ.2 h (Set.notMem_empty _) := by
  simp [heckeProj, heckeGen, heckeProjGen, h]

theorem heckeProj_C (c : ℤ) : heckeProj N (MvPolynomial.C c) = algebraMap ℤ (CuspForm.heckeAlgebra N 2 ∅) c := by
  simp [heckeProj]

theorem ringHom_ext_heckeProj {R : Type*} [Ring R] {f g : CuspForm.heckeAlgebra N 2 ∅ →+* R}
    (h : ∀ ℓ : Nat.Primes, f (heckeProjGen N ℓ) = g (heckeProjGen N ℓ)) :
    f.comp (heckeProj N) = g.comp (heckeProj N) := by
  apply MvPolynomial.ringHom_ext
  · intro c
    rw [RingHom.comp_apply, RingHom.comp_apply, heckeProj_C, eq_intCast, map_intCast, map_intCast]
  · intro ℓ
    simpa [heckeProj, heckeProjGen] using h ℓ

end ModularCurve

end

Statements phrased using this module (37)