Fourier coefficients of the Hecke operators at a prime power on M_k(N, χ) #
The Γ₀(N) Hecke ring acts on M_k(N, χ) through heckeRingHomCharSpace; at a prime p
the generator acts as the classical Tₚ (HeckeSlash/Nebentypus/Prime/Basic.lean), whose Fourier
coefficients are a_m(Tₚ F) = a_{pm}(F) + χ(p) p^{k−1} a_{m/p}(F)
(HeckeSlash/Recurrence.lean). Along the powers of a good prime p ∤ N the ring elements
T_{p^r} are the recurrence family heckeTGeneratorRecGamma0, with
T_{p^{r+2}} = Tₚ T_{p^{r+1}} − p S_p T_{p^r}, which on the character space reads
T_{p^{r+2}} = Tₚ ∘ T_{p^{r+1}} − χ(p) p^{k−1} • T_{p^r}
(HeckeSlash/Nebentypus/Prime/Recurrence.lean). Unwinding that recurrence on
coefficients gives the classical formula: writing c = χ(p) p^{k−1}, for every index m prime
to p,
a_{p^j m}(T_{p^r} F) = ∑_{i ≤ min j r} c^i · a_{p^{j+r−2i} m}(F),
the two-step recurrence between such sums being TauCeti.sum_range_min_add_two and its base
case TauCeti.sum_range_min_zero (Algebra/BigOperators/Finset/Range.lean),
the prime-power case of Diamond–Shurman Proposition 5.3.1, and in particular
a_m(T_{p^r} F) = a_{p^r m}(F). At a prime p ∣ N dividing the level the block degenerates to
the r-th power of Tₚ, and that same shift holds at every index m. The composite operators
are ordered products of these blocks (heckeTCompositeGamma0), so the two statements together
are the input for the coefficient formula of T_n read at a Fourier index m coprime to n.
Main results #
HeckeRing.GL2.qExpansion_coeff_prime_pow_mul_heckeRingHomCharSpace_heckeTGeneratorRecGamma0: the formula above.HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTGeneratorRecGamma0_of_not_dvd:a_m(T_{p^r} F) = a_{p^r m}(F)at an indexmprime top.HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTGeneratorRecGamma0_of_dvd_level: the same shifta_m(T_{p^r} F) = a_{p^r m}(F)at a primep ∣ Ndividing the level, now at every indexm.qExpansion_coeff_prime_pow_succ_mul_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0: the divisible-indexTₚrecurrence onS_k(N, χ), with no hypothesis on the index.- their cusp-form specialisations, named after the modular statements with
heckeRingHomCharSpacereplaced byheckeRingHomCuspCharSpace, transported along the inclusion of character spacescuspToModFormCharSpace.
Provenance #
Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08),
projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/FourierHecke.lean —
fourierCoeff_heckeT_ppow_period_one and fourierCoeff_heckeT_p_period_one, which state the
divisor-sum form a_m(T_{p^v} f) = ∑_{d ∣ gcd(m, p^v)} d^{k−1} χ(d) a_{m p^v / d²}(f) for the
source's concretely-defined heckeT_ppow. Here the operator is the Hecke ring's own recurrence
family acting through heckeRingHomCharSpace, so the formula is proved from the ring
recurrence and the prime case rather than from coset representatives, and it is stated at the
indices p^j m with m prime to p, where the divisor sum is the min sum above.
References #
- F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.3.1.
- T. Miyake, Modular forms, §4.5.
Tₚ at an index prime to p reads the coefficient at p m: the p ∣ m term of the
recurrence is absent.
Tₚ at an index divisible by p: a_{p^{j+1} m}(Tₚ G) = a_{p^{j+2} m}(G) + χ(p) p^{k−1} a_{p^j m}(G), the recurrence with both terms present.
The prime-power coefficient formula on M_k(N, χ). For a good prime p ∤ N, an index m
prime to p and all j, r, writing c = χ(p) p^{k−1},
a_{p^j m}(T_{p^r} F) = ∑_{i ≤ min j r} c^i · a_{p^{j+r−2i} m}(F)
(Diamond–Shurman Proposition 5.3.1 at a prime power).
At an index prime to p, T_{p^r} reads the coefficient at p^r m:
a_m(T_{p^r} F) = a_{p^r m}(F), the j = 0 case of the prime-power formula.
At a prime dividing the level, T_{p^r} shifts every Fourier coefficient by p^r:
a_m(T_{p^r} F) = a_{p^r m}(F), with no hypothesis on m. This is the bad-prime counterpart of
qExpansion_coeff_heckeRingHomCharSpace_heckeTGeneratorRecGamma0_of_not_dvd.
The cusp-form specialisations #
The prime-power coefficient formula on S_k(N, χ): the case of
qExpansion_coeff_prime_pow_mul_heckeRingHomCharSpace_heckeTGeneratorRecGamma0 at a cusp form,
whose q-expansion is that of the modular form underlying it.
The divisible-index recurrence for Tₚ on S_k(N, χ): the cusp-form counterpart of
qExpansion_coeff_prime_pow_succ_mul_heckeRingHomCharSpace_heckeTGeneratorGamma0, with no
hypothesis on m. Stated so that consumers on cuspFormCharSpace need neither a coercion nor
the full prime-power theorem's ¬ p ∣ m.
At an index prime to p, T_{p^r} reads the coefficient at p^r m, on S_k(N, χ).
At a prime dividing the level, T_{p^r} shifts every Fourier coefficient by p^r, on
S_k(N, χ).