The Fourier-coefficient recurrence for Tₚ, at every prime

HeckeSlash/Prime.lean writes the Hecke operator of the double coset Γ₁(N) · diag(1, p) · Γ₁(N) as a sum of slashes,

Tₚ f = ∑_{b < p} f ∣[k] !![1, b; 0, p] + (⟨p⟩ f) ∣[k] !![p, 0; 0, 1],

and the two q-expansion halves are already computed elsewhere: the upper-triangular sum reads off the coefficients of f along p ℕ (UpperTri/QExpansion.lean) and the rational diagonal slash is p ^ (k - 1) times a level raise (Diagonal/QExpansion.lean). This file adds them, turning the slash-level identity into Diamond–Shurman's recurrence on Fourier coefficients:

aₘ(Tₚ f) = a_{p m}(f) + p^{k−1} a_{m/p}(⟨p⟩ f),

and on a nebentypus space M_k(N, χ) with p ∤ N, where the diamond acts by the scalar χ(p),

aₘ(Tₚ f) = a_{p m}(f) + χ(p) p^{k−1} a_{m/p}(f).

One formula, both cases. As at the level of slashes, there is no case split on whether p divides the level: a_{m/p} is read as an explicit if p ∣ m, and at p ∣ N the zero-extended diamond ⟨p⟩ of DiamondOperators.lean vanishes, so the recurrence degenerates to aₘ(Tₚ f) = a_{p m}(f) — the operator modern papers write Uₚ. Following Miyake, Diamond–Shurman and Shimura, Uₚ is not a second operator, only this case of Tₚ.

The Nat division in a_{m/p} is guarded by that if: without it, m / p would silently round down at indices p ∤ m and name a coefficient the recurrence does not contain.

Main results

• HeckeRing.GL2.qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_prime and its cusp-form counterpart: the recurrence, uniformly at every prime.
• qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_mem_modFormCharSpace and its cusp-form counterpart: the recurrence on a nebentypus space at a good prime, with χ(p) in place of the diamond.
• HeckeRing.GL2.qExpansion_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_prime: the same identity between power series, the diamond term appearing as a PowerSeries.expand.
• HeckeRing.GL2.qExpansion_coeff_one_heckeSlashGamma1ModularFormEnd_diagCosetGamma1: a₁(Tₚ f) = a_p(f), and HeckeRing.GL2.eq_qExpansion_coeff_of_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_eq_smul: the Hecke eigenvalue of a normalized eigenvector is a_p.

Provenance

No code is transcribed. The Fourier-side statements of the AINTLIB LeanModularForms project live in HeckeRIngs/GL2/FourierHecke.lean (https://github.com/CBirkbeck/AINTLIB, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck) and carry the hypotheses f ∈ modFormCharSpace k χ and Nat.Coprime p N; those hypotheses are kept here rather than cleaned away. The derivation itself goes through this repository's own double-coset operator (HeckeSlash/Prime.lean) and the additivity of the q-expansion, not through a bespoke definition of Tₚ.

References

• F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.2.2 and equations (5.3)--(5.4).
• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5.
• T. Miyake, Modular forms, §4.5, Lemma 4.5.7: T(n) is defined for every n ≥ 1 with the nebentypus extended by χ(d) = 0 at (d, N) > 1, which is the convention under which the p ∣ N case below is Tₚ itself rather than a separate operator.

theorem HeckeRing.GL2.qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_prime {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1ModularFormEnd k (diagCosetGamma1 N p)) f)) = (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f) + if p ∣ m then ↑p ^ (k - 1) * (PowerSeries.coeff (m / p)) (UpperHalfPlane.qExpansion 1 ⇑((diamondOpNat k p) f)) else 0

The Fourier-coefficient recurrence for Tₚ on M_k(Γ₁(N)), at every prime.

aₘ(Tₚ f) = a_{p m}(f) + p^{k−1} a_{m/p}(⟨p⟩ f),

where the second term is present only when p ∣ m. There is no case split on the level: at p ∣ N the zero-extended diamond ⟨p⟩ vanishes and the recurrence degenerates to aₘ(Tₚ f) = a_{p m}(f).

theorem HeckeRing.GL2.qExpansion_coeff_heckeSlashGamma1CuspFormEnd_diagCosetGamma1_of_prime {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1CuspFormEnd k (diagCosetGamma1 N p)) f)) = (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f) + if p ∣ m then ↑p ^ (k - 1) * (PowerSeries.coeff (m / p)) (UpperHalfPlane.qExpansion 1 ⇑((diamondOpCuspNat k p) f)) else 0

The Fourier-coefficient recurrence for Tₚ on S_k(Γ₁(N)), at every prime — the same formula, with the cusp-form diamond operator.

theorem HeckeRing.GL2.qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_mem_modFormCharSpace {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (h : p.Coprime N) (χ : (ZMod N)ˣ →* ℂˣ) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1ModularFormEnd k (diagCosetGamma1 N p)) f)) = (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f) + if p ∣ m then ↑(χ (ZMod.unitOfCoprime p h)) * ↑p ^ (k - 1) * (PowerSeries.coeff (m / p)) (UpperHalfPlane.qExpansion 1 ⇑f) else 0

Diamond–Shurman's recurrence on a nebentypus space M_k(N, χ) at a good prime. For p ∤ N the diamond acts by the scalar χ(p), so

aₘ(Tₚ f) = a_{p m}(f) + χ(p) p^{k−1} a_{m/p}(f).

theorem HeckeRing.GL2.qExpansion_coeff_heckeSlashGamma1CuspFormEnd_diagCosetGamma1_of_mem_cuspFormCharSpace {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (h : p.Coprime N) (χ : (ZMod N)ˣ →* ℂˣ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1CuspFormEnd k (diagCosetGamma1 N p)) f)) = (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f) + if p ∣ m then ↑(χ (ZMod.unitOfCoprime p h)) * ↑p ^ (k - 1) * (PowerSeries.coeff (m / p)) (UpperHalfPlane.qExpansion 1 ⇑f) else 0

Diamond–Shurman's recurrence on a nebentypus space S_k(N, χ) at a good prime.

theorem HeckeRing.GL2.qExpansion_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_prime {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1ModularFormEnd k (diagCosetGamma1 N p)) f) = (PowerSeries.mk fun (m : ℕ) => (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f)) + ↑p ^ (k - 1) • (PowerSeries.expand p ⋯) (UpperHalfPlane.qExpansion 1 ⇑((diamondOpNat k p) f))

The recurrence as an identity of power series. The q-expansion of Tₚ f is the subseries of f along p ℕ, reindexed, plus p^{k−1} times the p-fold expansion of the q-expansion of ⟨p⟩ f.

theorem HeckeRing.GL2.qExpansion_heckeSlashGamma1CuspFormEnd_diagCosetGamma1_of_prime {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1CuspFormEnd k (diagCosetGamma1 N p)) f) = (PowerSeries.mk fun (m : ℕ) => (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f)) + ↑p ^ (k - 1) • (PowerSeries.expand p ⋯) (UpperHalfPlane.qExpansion 1 ⇑((diamondOpCuspNat k p) f))

The recurrence as an identity of power series, on cusp forms.

theorem HeckeRing.GL2.qExpansion_coeff_one_heckeSlashGamma1ModularFormEnd_diagCosetGamma1 {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1ModularFormEnd k (diagCosetGamma1 N p)) f)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f)

The first coefficient of Tₚ f is the p-th coefficient of f, at every prime and every level: p ∤ 1, so the diamond term of the recurrence is absent. This is what turns a Hecke eigenvalue into a Fourier coefficient.

theorem HeckeRing.GL2.qExpansion_coeff_one_heckeSlashGamma1CuspFormEnd_diagCosetGamma1 {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((heckeSlashGamma1CuspFormEnd k (diagCosetGamma1 N p)) f)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f)

The first coefficient of Tₚ f on cusp forms.

theorem HeckeRing.GL2.eq_qExpansion_coeff_of_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_eq_smul {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} {c : ℂ} (hc : (heckeSlashGamma1ModularFormEnd k (diagCosetGamma1 N p)) f = c • f) (h1 : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f) = 1) : c = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f)

The Hecke eigenvalue of a normalized eigenvector is its p-th Fourier coefficient. If Tₚ f = c f and f is normalized (a₁(f) = 1), then c = a_p(f). This is the identity that lets eigenvalue systems be read off q-expansions.

theorem HeckeRing.GL2.eq_qExpansion_coeff_of_heckeSlashGamma1CuspFormEnd_diagCosetGamma1_eq_smul {N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} {c : ℂ} (hc : (heckeSlashGamma1CuspFormEnd k (diagCosetGamma1 N p)) f = c • f) (h1 : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f) = 1) : c = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f)

The Hecke eigenvalue of a normalized eigenvector, on cusp forms.