The Fourier coefficient of T_n F at an index coprime to n

The composite element heckeTCompositeGamma0 N n of the Γ₀(N) Hecke ring is the ordered product of the prime-power blocks heckeTGeneratorRecGamma0 N p (v_p n) over the primes of n (HeckeRing/GL2/Gamma0/Diagonal/Composite.lean), and each block reads the coefficient at p^{v_p n} m — at a good prime when p ∤ m, and at a prime dividing the level unconditionally (HeckeSlash/Nebentypus/Prime/Power.lean). Peeling the blocks off one at a time therefore gives, for n ≠ 0 and m coprime to n,

a_m(T_n F) = a_{m n}(F).

Coprimality of m and n is what makes the formula this simple: each block meets an index prime to its own prime, so only the leading term of the prime-power formula survives. At m = 1 it says a_1(T_n F) = a_n(F); read on a Hecke eigenvector, where T_n F = λ_n F, that is a_n(F) = λ_n a_1(F) — the coefficient form of the eigenvalue system (Newforms/Coefficient.lean).

The same peeling, run on the operators rather than on the coefficients, shows that a subspace of S_k(N, χ) stable under every prime generator T_p is stable under every T_n: each block is a polynomial in T_p and the scalar coset T(p, p), which acts on S_k(N, χ) by a scalar.

Main results

• HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTCompositeGamma0_mem_of_forall_prime_dvd: a subspace of S_k(N, χ) stable under T_p at every prime p ∣ n is stable under T_n.
• HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_coprime: a_m(T_n F) = a_{m n}(F) for n ≠ 0 and m coprime to n, on M_k(N, χ).
• HeckeRing.GL2.qExpansion_coeff_one_heckeRingHomCharSpace_heckeTCompositeGamma0: its m = 1 case a_1(T_n F) = a_n(F), the normalisation reading an arbitrary coefficient of F off the first coefficient of T_n F.
• HeckeRing.GL2.qExpansion_coeff_heckeRingHomCuspCharSpace_heckeTCompositeGamma0_of_coprime: its specialisation to S_k(N, χ), along cuspToModFormCharSpace.

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_n_period_one, the divisor-sum formula at a general index for the source's concretely-defined heckeT_n, which at indices coprime to n collapses to the single coefficient below. Here the operator is the Hecke ring's composite element heckeTCompositeGamma0 acting through heckeRingHomCharSpace, so the proof peels its prime-power blocks instead of summing over divisors.

References

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

theorem HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_coprime {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {n : ℕ} (hn : n ≠ 0) (F : ↥(modFormCharSpace k χ)) {m : ℕ} (hmn : m.Coprime n) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑↑(((heckeRingHomCharSpace k χ) (heckeTCompositeGamma0 N n)) F)) = (PowerSeries.coeff (m * n)) (UpperHalfPlane.qExpansion 1 ⇑↑F)

The Fourier coefficient of T_n F at an index coprime to n. For n ≠ 0 and m coprime to n, the Hecke ring's composite element reads the coefficient at m n: a_m(T_n F) = a_{m n}(F). No hypothesis relating n to the level is needed: the blocks at the primes dividing N shift every coefficient.

theorem HeckeRing.GL2.qExpansion_coeff_one_heckeRingHomCharSpace_heckeTCompositeGamma0 {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {n : ℕ} (hn : n ≠ 0) (F : ↥(modFormCharSpace k χ)) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑↑(((heckeRingHomCharSpace k χ) (heckeTCompositeGamma0 N n)) F)) = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑↑F)

The first Fourier coefficient of T_n F is the n-th coefficient of F: a_1(T_n F) = a_n(F), the m = 1 case of qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_coprime. It is this normalisation that lets an arbitrary coefficient of F be read off a first coefficient.

theorem HeckeRing.GL2.qExpansion_coeff_heckeRingHomCuspCharSpace_heckeTCompositeGamma0_of_coprime {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {n : ℕ} (hn : n ≠ 0) (F : ↥(cuspFormCharSpace k χ)) {m : ℕ} (hmn : m.Coprime n) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑↑(((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N n)) F)) = (PowerSeries.coeff (m * n)) (UpperHalfPlane.qExpansion 1 ⇑↑F)

The Fourier coefficient of T_n F at an index coprime to n, on S_k(N, χ): the case of qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_coprime at a cusp form, transported along the inclusion of character spaces.

theorem HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTCompositeGamma0_mem_of_forall_prime_dvd {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {V : Submodule ℂ ↥(cuspFormCharSpace k χ)} {n : ℕ} (hV : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ F ∈ V, ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) F ∈ V) {F : ↥(cuspFormCharSpace k χ)} (hF : F ∈ V) : ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N n)) F ∈ V

A subspace of S_k(N, χ) stable under the prime generators T_p at every prime p ∣ n is stable under T_n. The composite element heckeTCompositeGamma0 N n is a product of the prime-power blocks T_{p^v} over the primes p ∣ n, each a polynomial in T_p and the scalar coset T(p, p); the latter acts on S_k(N, χ) by the scalar χ(p) p^{k-2} when p ∤ N and is 0 when p ∣ N, so it preserves every subspace.