Eigenvectors of Hecke operators at bad primes

At a bad prime p ∣ N, the operator is the alias U_p = T_p, and the level-supported coefficient characterization in HeckeSlash/LevelSupported.lean becomes the familiar criterion U_p f = c f ↔ a_{pm}(f) = c a_m(f). This is the bad-prime counterpart of the good-prime criterion in HeckeSlash/Nebentypus/Eigenvector.lean. On a nebentypus space the two criteria combine into one statement at every prime: with the nebentypus extended by zero, χ(p) = 0 for p ∣ N (Mathlib's MulChar.ofUnitHom),

T_p F = c F ↔ a_{pm}(F) = c a_m(F) − χ(p) p^{k−1} a_{m/p}(F) for every m,

the last term present only when p ∣ m. This turns the prime-power and coprime-product recurrences of a normalized form into eigenvector equations at every prime.

Main results

• HeckeRing.GL2.heckeUNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul and its cusp-form counterpart give the criterion in the standard bad-prime notation.
• HeckeRing.GL2.heckeTNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul_ofUnitHom and its cusp-form counterpart give the criterion at every prime, with the zero-extended nebentypus.

References

• F. Diamond and J. Shurman, A first course in modular forms, Propositions 5.2.1–5.2.2 and Proposition 5.8.5.
• T. Miyake, Modular forms, §4.5, Lemma 4.5.7.

theorem HeckeRing.GL2.heckeUNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul {N p : ℕ} [NeZero N] (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {F : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (c : ℂ) : (heckeUNat k p hp hpN) F = c • F ↔ ∀ (m : ℕ), (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑F) = c * (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑F)

The bad-prime coefficient characterization U_p F = c • F, on modular forms. For a prime p ∣ N, the relation holds exactly when a_{pm}(F) = c a_m(F) for every m.

theorem HeckeRing.GL2.heckeUCuspNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul {N p : ℕ} [NeZero N] (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (c : ℂ) : (heckeUCuspNat k p hp hpN) F = c • F ↔ ∀ (m : ℕ), (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑F) = c * (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑F)

The bad-prime coefficient characterization U_p F = c • F, on cusp forms. For a prime p ∣ N, the relation holds exactly when a_{pm}(F) = c a_m(F) for every m.

The criterion at every prime

theorem HeckeRing.GL2.heckeTNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul_ofUnitHom {N p : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (hp : Nat.Prime p) {F : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hF : F ∈ modFormCharSpace k χ) (c : ℂ) : (heckeTNat k p) F = c • F ↔ ∀ (m : ℕ), (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑F) = c * (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑F) - if p ∣ m then (MulChar.ofUnitHom χ) ↑p * ↑p ^ (k - 1) * (PowerSeries.coeff (m / p)) (UpperHalfPlane.qExpansion 1 ⇑F) else 0

The coefficient characterization of T_p F = c • F at every prime, on M_k(N, χ). With the nebentypus extended by zero to the residues not prime to N, the relation holds exactly when a_{pm}(F) = c a_m(F) − χ(p) p^{k−1} a_{m/p}(F) for every m, the last term present only when p ∣ m. At a good prime this is heckeTNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul; at a prime dividing the level χ(p) = 0 and it is heckeUNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul.

theorem HeckeRing.GL2.heckeTCuspNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul_ofUnitHom {N p : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (hp : Nat.Prime p) {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hF : F ∈ cuspFormCharSpace k χ) (c : ℂ) : (heckeTCuspNat k p) F = c • F ↔ ∀ (m : ℕ), (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑F) = c * (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑F) - if p ∣ m then (MulChar.ofUnitHom χ) ↑p * ↑p ^ (k - 1) * (PowerSeries.coeff (m / p)) (UpperHalfPlane.qExpansion 1 ⇑F) else 0

The coefficient characterization of T_p F = c • F at every prime, on S_k(N, χ): the cusp-form case of heckeTNat_eq_smul_iff_forall_qExpansion_coeff_prime_mul_ofUnitHom.