Eigen at the primes is eigen at the composite indices

A cusp form of nebentypus χ that is an eigenvector of the Γ₀(N) Hecke ring at the generator T_p of every prime p ∤ N is an eigenvector at heckeTCompositeGamma0 N n for every n coprime to N. Eigen-ness away from the level is therefore determined by the good primes alone, which is what makes a full eigenvalue system available from prime data: a coefficient recurrence, a diagonalisation or a spectral argument each produce the eigen-property one prime at a time.

Two identities carry it to the composite indices. heckeTCompositeGamma0_prime_pow identifies the composite at a prime power with the Diamond–Shurman recurrence family, and heckeTCompositeGamma0_mul_of_coprime factors a general index into its prime powers. Since heckeRingHomCuspCharSpace is a ring homomorphism, the ring elements acting on a fixed form by a scalar are closed under products, which carries the eigen-property along both; along the prime powers the recurrence contributes the term (p • S_p) · T_{p^r}, whose scalar action is the nebentypus (heckeRingHomCuspCharSpace_heckeTGeneratorRecGamma0_succ_succ).

If the form is an eigenvector at the bad primes as well, the same argument covers every positive index. At a bad prime the recurrence family is a power of T_p; the same coprime multiplication law then assembles arbitrary mixtures of good and bad prime-power blocks.

Main results

• HeckeRing.GL2.exists_smul_heckeTCompositeGamma0_of_forall_prime_of_coprime: the eigen-property spreads from the good primes to every good index.
• HeckeRing.GL2.exists_smul_heckeTCompositeGamma0_of_forall_prime: eigen-relations at every prime, including those dividing the level, spread to every positive index.

References

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

theorem HeckeRing.GL2.exists_smul_heckeTCompositeGamma0_of_forall_prime_of_coprime {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {F : ↥(cuspFormCharSpace k χ)} (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) F = c • F) (n : ℕ) (hnN : n.Coprime N) : ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N n)) F = c • F

Eigen at every good prime is eigen at every good index. If the Hecke-ring generator at every prime p ∤ N acts on F ∈ S_k(N, χ) by a scalar, then so does heckeTCompositeGamma0 N n at every n coprime to N.

This is what makes an eigenvalue system away from the level available from prime data: a form satisfying the hypothesis has a scalar at each good index, and choosing one at each index is a complete eigenvalue system in the sense EigenformAwayFromLevel asks for.

theorem HeckeRing.GL2.exists_smul_heckeTCompositeGamma0_of_forall_prime {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {F : ↥(cuspFormCharSpace k χ)} (h : ∀ (p : ℕ), Nat.Prime p → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) F = c • F) (n : ℕ) (hn : n ≠ 0) : ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTCompositeGamma0 N n)) F = c • F

Eigen at every prime is eigen at every positive index. If the Hecke-ring generator at every prime acts on F ∈ S_k(N, χ) by a scalar, then so does heckeTCompositeGamma0 N n for every positive index n.

At a good prime the prime-power blocks follow the Diamond–Shurman recurrence. At a prime dividing the level the scalar term vanishes, so the block is a power of T_p. Coprime products, including products of good and bad prime powers, are assembled by heckeTCompositeGamma0_mul_of_coprime.