`Definitions/Def_CuspForm_IntegralStructure.lean`

definition module

Integral structure on cusp forms for $Γ_{0} (N)$

Two declarations about the space CuspForm (CongruenceSubgroup.Gamma0 N) k of weight-k cusp forms on \Gamma_0(N), for arbitrary N : \mathbb{N} and k : \mathbb{Z}, phrased throughout in terms of the project's q-expansion coefficients ModularFormClass.qCoeff f n (the n-th coefficient of the expansion at the cusp \infty in q = e^{2\pi i\tau}, width 1 — the same coefficients used in the project's normalised-eigenform and Hecke dictionaries).

CuspForm.intLattice N k is the \mathbb{Z}-submodule of CuspForm (CongruenceSubgroup.Gamma0 N) k generated (as a \mathbb{Z}-span) by the set of those cusp forms f such that for every n : \mathbb{N} there is an m : \mathbb{Z} with a_n(f) = m in \mathbb{C}; that is, the span of the forms all of whose Fourier coefficients at \infty are rational integers. Note that the spanning set is cut out by a condition on the coefficients only, and that the span is taken to make the result a submodule.

CuspForm.HasIntegralStructure N k is a proposition: the \mathbb{C}-span of the underlying set of CuspForm.intLattice N k is all of CuspForm (CongruenceSubgroup.Gamma0 N) k (equality with \top). Equivalently, S_k(\Gamma_0(N)) is spanned over \mathbb{C} by cusp forms with integral q-expansions, i.e. S_k(\Gamma_0(N);\mathbb{Z}) \otimes_{\mathbb{Z}} \mathbb{C} = S_k(\Gamma_0(N)). This is a definition only: the module records the statement so that results requiring integrality of Hecke eigenvalues can carry it as one named hypothesis, and nothing here asserts it for any particular N and k. Classically it holds for all N \ge 1 and all k, by the q-expansion principle.

Relation to Mathlib

Both declarations are the project's own; Mathlib supplies the space CuspForm for CongruenceSubgroup.Gamma0 N, the submodule and span machinery, but no notion of an integral lattice of cusp forms or of a rational/integral structure on such spaces.

Where it is used

The predicate CuspForm.HasIntegralStructure is carried as an explicit hypothesis by the parts of the development that need Hecke eigenvalues a_\ell(f) of a normalised eigenform to be algebraic integers, which is what feeds the construction of the mod-\ell representation attached to a Frey package and the residual modularity statements used in the Frey–Serre–Ribet step.

References

G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Theorem 3.52
F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §6.5

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

9 lines
2 declarations
used in the statements of 104 theorems and imported by 128 proofs
imports 1 definition modules

Source file: Definitions/Def_CuspForm_IntegralStructure.lean

Imports

Def_FLTPrelim_Modularity

Imported by

Source

import Definitions.Def_FLTPrelim_Modularity

def CuspForm.intLattice (N : ℕ) (k : ℤ) : Submodule ℤ (CuspForm (CongruenceSubgroup.Gamma0 N) k) :=
  Submodule.span ℤ {f | ∀ n : ℕ, ∃ m : ℤ, ModularFormClass.qCoeff f n = (m : ℂ)}

def CuspForm.HasIntegralStructure (N : ℕ) (k : ℤ) : Prop :=
  Submodule.span ℂ ((CuspForm.intLattice N k : Submodule ℤ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) :
    Set (CuspForm (CongruenceSubgroup.Gamma0 N) k)) = ⊤

Definitions/Def_CuspForm_IntegralStructure.lean

Integral structure on cusp forms for Γ0​(N)