Fourier coefficients of composite Hecke operators

For every nonzero index n, each positive Fourier coefficient of the action of the composite Hecke-ring element T_n on M_k(N, χ) has the classical divisor-sum formula

a_m(T_n F) = ∑ d ∣ gcd(m,n), χ(d) d^{k−1} a_{mn/d²}(F).

The character is written through MulChar.ofUnitHom, Mathlib's zero-extension of a unit homomorphism to a Dirichlet character. A divisor sharing a factor with the level contributes nothing: its scalar generator S_d vanishes (heckeTScalarGamma0_of_not_coprime) and so does χ(d). The sum therefore runs over all divisors of gcd(m, n), and no hypothesis relates n to the level.

Main results

• HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_ne_zero: the divisor-sum formula at positive indices on M_k(N, χ).
• HeckeRing.GL2.qExpansion_coeff_heckeRingHomCuspCharSpace_heckeTCompositeGamma0: its cusp-form specialization.

Provenance

The statement is the coefficient formula fourierCoeff_heckeT_n_period_one from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08), file LeanModularForms/HeckeRIngs/GL2/FourierHecke.lean.

References

• F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.3.1.
• T. Miyake, Modular forms, §4.5.

theorem HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_ne_zero {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {n : ℕ} (hn : n ≠ 0) (F : ↥(modFormCharSpace k χ)) {m : ℕ} (hm : m ≠ 0) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑↑(((heckeRingHomCharSpace k χ) (heckeTCompositeGamma0 N n)) F)) = ∑ d ∈ (m.gcd n).divisors, (MulChar.ofUnitHom χ) ↑d * ↑d ^ (k - 1) * (PowerSeries.coeff (m * n / d ^ 2)) (UpperHalfPlane.qExpansion 1 ⇑↑F)

The divisor-sum formula for the composite Hecke action on M_k(N, χ). If n is nonzero, then

a_m(T_n F) = ∑ d ∣ gcd(m,n), χ(d) d^{k−1} a_{mn/d²}(F).

Here χ(d) is Mathlib's zero-extension MulChar.ofUnitHom χ, which vanishes at a divisor sharing a factor with N; such divisors contribute nothing to the sum.

theorem HeckeRing.GL2.qExpansion_coeff_heckeRingHomCuspCharSpace_heckeTCompositeGamma0 {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {n : ℕ} (hn : n ≠ 0) (F : ↥(cuspFormCharSpace k χ)) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑↑(((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N n)) F)) = ∑ d ∈ (m.gcd n).divisors, (MulChar.ofUnitHom χ) ↑d * ↑d ^ (k - 1) * (PowerSeries.coeff (m * n / d ^ 2)) (UpperHalfPlane.qExpansion 1 ⇑↑F)

The divisor-sum formula on S_k(N, χ). This is the modular-form formula transported along the inclusion cuspToModFormCharSpace.