Modular forms — Hecke theory, newforms, and L-functions
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremThe valence formula at general level#
for a nonzero weight-k form on a finite-index
Γ ≤ SL(2, ℤ), the interior orders — weighted by 2 / |Stab_Γ P| — together with the orders
indexed by the cusp translation orbits add up to k · [SL(2, ℤ) : Γ] / 12.
This is valence_formula_finiteIndex_norm with its cusp term, an order at ∞ on the norm,
distributed over the cusps of Γ.
TauCeti.ModularForm.valence_formula_finiteIndex.{u_1} {F : Type u_1} [FunLike F UpperHalfPlane ℂ]
{k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex]
[ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F)
(hf : ⇑f ≠ 0) :
∑ᶠ (o :
MulAction.orbitRel.Quotient (↥(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ))
UpperHalfPlane),
TauCeti.ModularForm.weightedOrderOfVanishingOnSubgroupOrbit f o +
∑ c, ↑(TauCeti.ModularForm.orderAtCuspTranslationOrbit f c) =
↑k *
↑(Nat.card
(↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸
(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).subgroupOf
(Matrix.SpecialLinearGroup.mapGL ℝ).range)) /
12
Lean
Formalized in Tau Ceti as TauCeti.ModularForm.valence_formula_finiteIndex.
Sources
TheoremA newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f)#
A newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue
a_p(f) (Atkin–Lehner; Li; Diamond–Shurman, Theorem 5.8.2; Miyake, Theorem 4.6.13). Together
with the good eigensystem this makes a newform a full Hecke eigenform (Newform.toEigenform).
The statement is on the bad-prime operator heckeUCuspNat, matching the U_p-spelled API of
HeckeSlash/BadPrime; Newform.heckeTCuspNat_eq_qExpansion_coeff_smul is the statement at
every prime.
HeckeRing.GL2.Newform.heckeUCuspNat_eq_qExpansion_coeff_smul {N : ℕ} [NeZero N] {k : ℤ}
(f : HeckeRing.GL2.Newform N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) :
(HeckeRing.GL2.heckeUCuspNat k p hp hpN) f.toCuspForm =
(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) • f.toCuspForm
Lean
Formalized in Tau Ceti as HeckeRing.GL2.Newform.heckeUCuspNat_eq_qExpansion_coeff_smul.
Sources
- Tau Ceti documentation:
HeckeRing.GL2.Newform.heckeUCuspNat_eq_qExpansion_coeff_smul - Source of
HeckeRing.GL2.Newform.heckeUCuspNat_eq_qExpansion_coeff_smulin TauCeti/NumberTheory/ModularForms/Newforms/FullEigenform.lean - Tau Ceti roadmap status: Modular forms — Hecke theory, newforms, and L-functions
Uses 7 · Used by 3
SL(2, ℤ) · The Main Lemma, per character (Miyake, Lemma 4.6.8; Diamond–Shurman, Theorem 5.7.1) · The Petersson adjoint formula in the second argument · Shimura's commutativity criterion (Proposition 3.8 of [Shimura][shimura1971]) · Shimura's decomposition of a double coset into right cosets · Sturm bound for subgroups of GL(2, ℝ) of finite relative index in SL(2, ℤ) with discrete strict periods · The third isomorphism theorem for coset spacesTheoremHeckeRing.GL2.Newform.L_eulerProduct#
Finite Euler products converge to Mathlib's ModularForm.L for a newform.
HeckeRing.GL2.Newform.L_eulerProduct {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k)
(hk : 0 < k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) :
Filter.Tendsto
(fun n =>
∏ p ∈ n.primesBelow,
(1 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * ↑p ^ (-s) +
f.dirichletLift ↑p * ↑p ^ (k - 1) * ↑p ^ (-2 * s))⁻¹)
Filter.atTop (nhds (ModularForm.L hk f.toCuspForm s))
TheoremThe coefficient field of a newform of weight at least two is a number field#
TauCeti.numberField_CoefficientField {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k)
(hk : 2 ≤ k) : NumberField ↥(TauCeti.CoefficientField f)
Uses 7
U_p at every prime p dividing the level, with eigenvalue a_p(f) · Manin's lemma · Periods determine a cusp form · Shimura's commutativity criterion (Proposition 3.8 of [Shimura][shimura1971]) · Shimura's decomposition of a double coset into right cosets · TauCeti.ModularSymbols · TauCeti.ModularSymbols.periodMap
TheoremThe cusp–Eisenstein decomposition of M_k(N, χ)#
in weight k ≥ 3, the span of the
Eisenstein series of nebentypus χ is a complement of the image of S_k(N, χ) in M_k(N, χ).
TauCeti.isCompl_eisensteinSubspace_range_cuspToModFormCharSpace {N k : ℕ} [NeZero N]
(χ : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) :
IsCompl (TauCeti.eisensteinSubspace χ hk) (TauCeti.cuspToModFormCharSpace (↑k) χ).range
Lean
Formalized in Tau Ceti as TauCeti.isCompl_eisensteinSubspace_range_cuspToModFormCharSpace.
Sources
- Tau Ceti documentation:
TauCeti.isCompl_eisensteinSubspace_range_cuspToModFormCharSpace - Source of
TauCeti.isCompl_eisensteinSubspace_range_cuspToModFormCharSpacein TauCeti/NumberTheory/ModularForms/EisensteinSeries/Dimension.lean - Tau Ceti roadmap status: Modular forms — Hecke theory, newforms, and L-functions
AbbreviationTauCeti.ModularSymbols#
The module of modular symbols 𝕄_w(Γ; R) = (Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²))_Γ of weight
w + 2 for a subgroup Γ ≤ SL(2, ℤ), with coefficients in R: the Γ-coinvariants of the
degree-zero divisors on the cusps tensored with the binary forms of degree w.
This is an abbreviation for the coinvariants, so that their universal property
(Representation.Coinvariants.lift, Representation.Coinvariants.hom_ext) applies directly.
TauCeti.ModularSymbols.{u_1} (R : Type u_1) [CommRing R]
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (w : ℕ) : Type u_1
DefinitionTauCeti.ModularSymbols.periodMap#
The period map S_k(Γ) →ₗ[ℂ] (𝕄_w(Γ; R) →ₗ[R] ℂ) for k = w + 2: a cusp form f on
Γ is sent to the R-linear functional on the modular symbols induced by its raw period
pairing, so that {α, β} ⊗ P ↦ ∫_β^α f(z) P(z, 1) dz. For R = ℤ this is
the pairing of cusp forms with the integral modular symbols.
TauCeti.ModularSymbols.periodMap.{u_1} (R : Type u_1) [CommRing R] [Algebra R ℂ]
(Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] {k : ℤ} {w : ℕ}
(hk : k = ↑w + 2) :
CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k →ₗ[ℂ]
TauCeti.ModularSymbols R Γ w →ₗ[R] ℂ
Uses 2 · Used by 3
TheoremPeriods determine a cusp form#
For a finite-index subgroup of SL(2, ℤ) and weight
k = w + 2 ≥ 2, the period map into the dual of the modular symbols over R is injective.
In particular this applies to the integral modular symbols (R = ℤ).
TauCeti.ModularSymbols.periodMap_injective.{u_1} {R : Type u_1} [CommRing R] [Algebra R ℂ]
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {w : ℕ}
(hk : k = ↑w + 2) : Function.Injective ⇑(TauCeti.ModularSymbols.periodMap R Γ hk)
Uses 3 · Used by 1
DefinitionThe Atkin–Li pseudo-eigenvalue#
The Atkin–Li pseudo-eigenvalue λ_Q(f) of a newform f at an exact divisor Q of the
level: the scalar with 𝒲_Q f = λ_Q(f) • g, where 𝒲_Q is the slash by the Atkin–Li matrix
atkinLiMatrix N Q normalized by (√Q) ^ (2 - k) and g = f.atkinLehnerTransform h is the
transported newform. Since g has first Fourier coefficient 1, it is the first Fourier
coefficient of 𝒲_Q f.
HeckeRing.GL2.Newform.atkinLehnerPseudoEigenvalue {N Q : ℕ} [NeZero N] {k : ℤ}
(f : HeckeRing.GL2.Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) : ℂ
Lean
Formalized in Tau Ceti as HeckeRing.GL2.Newform.atkinLehnerPseudoEigenvalue.
Sources
DefinitionThe cusps of Γ₀(N)#
The cusps of Γ₀(N) are in bijection with the pairs (g, x) of a divisor g of N
and a unit x modulo gcd(g, N / g). The cusp γ • ∞ corresponds to the label of γ
(gamma0CuspOrbitEquiv_cuspOrbitOfSL2Z).
TauCeti.gamma0CuspOrbitEquiv (N : ℕ) [NeZero N] :
(Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma0 N)).CuspOrbit ≃
(g : ↥N.divisors) × (ZMod ((↑g).gcd (N / ↑g)))ˣ
TheoremThe Main Lemma, per character (Miyake, Lemma 4.6.8; Diamond–Shurman, Theorem 5.7.1)#
a
cusp form in S_k(Γ₁(N), χ) whose Fourier coefficients vanish at every index coprime to N
lies in the old subspace. It is a sum, over the primes p ∣ N, of forms of the same nebentypus
supported on the multiples of p, and each of those is old.
TauCeti.mem_cuspFormsOld_of_forall_coprime_qExpansion_coeff_eq_zero {N : ℕ} [NeZero N] {k : ℤ}
{χ : (ZMod N)ˣ →* ℂˣ}
{f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k}
(hf : f ∈ TauCeti.cuspFormCharSpace k χ)
(hvan : ∀ (n : ℕ), n.Coprime N → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) :
f ∈ TauCeti.cuspFormsOld N k
Lean
Formalized in Tau Ceti as TauCeti.mem_cuspFormsOld_of_forall_coprime_qExpansion_coeff_eq_zero.
Sources
Uses 1 · Used by 3
TheoremManin's lemma#
The degree-zero divisors on the cusps are spanned by the unimodular
symbols [g∞] - [g0], g ∈ SL(2, ℤ), that is, by the SL(2, ℤ)-translates of [∞] - [0].
TauCeti.ModularSymbols.degreeZero_eq_span_unimodular.{u_1} {R : Type u_1} [Ring R] :
TauCeti.ModularSymbols.degreeZero R =
Submodule.span R
(Set.range fun g =>
MonoidAlgebra.single ((Matrix.SpecialLinearGroup.mapGL ℚ) g • OnePoint.infty) 1 -
MonoidAlgebra.single ((Matrix.SpecialLinearGroup.mapGL ℚ) g • ↑0) 1)
Lean
Formalized in Tau Ceti as TauCeti.ModularSymbols.degreeZero_eq_span_unimodular.
Other forms
Manin's lemma, inside Div⁰(ℙ¹(ℚ)). Formalized in Tau Ceti as TauCeti.ModularSymbols.span_degreeZeroRep_eq_top.
TauCeti.ModularSymbols.span_degreeZeroRep_eq_top.{u_1} {R : Type u_1} [Ring R] :
Submodule.span R
(Set.range fun g =>
((TauCeti.ModularSymbols.degreeZeroRep R) g)
⟨MonoidAlgebra.single OnePoint.infty 1 - MonoidAlgebra.single (↑0) 1, ⋯⟩) =
⊤
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.