The prime-power recurrence of the Hecke ring on the character spaces

For p coprime to N the Hecke ring satisfies T_{p^{r+2}} = Tₚ T_{p^{r+1}} − p S_p T_{p^r} (heckeTGeneratorRecGamma0_succ_succ). The scalar coset S_p acts on the character space by χ(p) p^{k−2} (heckeRingHomCharSpace_heckeTScalarGamma0, Nebentypus/Scalar.lean), so p • S_p acts by χ(p) p^{k−1} and transporting the recurrence along the ring homomorphism gives T_{p^{r+2}} = Tₚ ∘ T_{p^{r+1}} − χ(p) p^{k−1} • T_{p^r} on M_k(N, χ) and on S_k(N, χ).

Prime/Power.lean consumes the pointwise forms to compute Fourier coefficients of T_{p^r}, and Newforms/RingEigenvalue.lean to derive the recurrence for the eigenvalues of a newform.

Main results

• HeckeRing.GL2.heckeRingHomCharSpace_heckeTGeneratorRecGamma0_succ_succ and its pointwise form ..._succ_succ_apply: the two-step recurrence on M_k(N, χ).
• HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTGeneratorRecGamma0_succ_succ and its pointwise form ..._succ_succ_apply: the same recurrence on S_k(N, χ).

theorem HeckeRing.GL2.heckeRingHomCharSpace_heckeTGeneratorRecGamma0_succ_succ {N : ℕ} [NeZero N] {p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (hp : 0 < p) (hpN : p.Coprime N) (r : ℕ) : (heckeRingHomCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 2)) = (heckeRingHomCharSpace k χ) (heckeTGeneratorGamma0 N p) * (heckeRingHomCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 1)) - (↑(χ (ZMod.unitOfCoprime p hpN)) * ↑p ^ (k - 1)) • (heckeRingHomCharSpace k χ) (heckeTGeneratorRecGamma0 N p r)

The recurrence, transported to the character space. For p coprime to N, T_{p^{r+2}} = Tₚ ∘ T_{p^{r+1}} − χ(p) p^{k−1} • T_{p^r} as endomorphisms of M_k(N, χ): the image of heckeTGeneratorRecGamma0_succ_succ under the ring homomorphism, with the scalar coset acting by χ(p) p^{k−2} (heckeRingHomCharSpace_heckeTScalarGamma0), so that p • S_p acts by χ(p) p^{k−1}. Only positivity of p is used.

theorem HeckeRing.GL2.heckeRingHomCharSpace_heckeTGeneratorRecGamma0_succ_succ_apply {N : ℕ} [NeZero N] {p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (hp : 0 < p) (hpN : p.Coprime N) (F : ↥(modFormCharSpace k χ)) (r : ℕ) : ((heckeRingHomCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 2))) F = ((heckeRingHomCharSpace k χ) (heckeTGeneratorGamma0 N p)) (((heckeRingHomCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 1))) F) - (↑(χ (ZMod.unitOfCoprime p hpN)) * ↑p ^ (k - 1)) • ((heckeRingHomCharSpace k χ) (heckeTGeneratorRecGamma0 N p r)) F

The recurrence at a form: heckeRingHomCharSpace_heckeTGeneratorRecGamma0_succ_succ evaluated. This is the pointwise interface — the shape the coefficient formula of Prime/Power.lean and the eigenvalue recurrence of Newforms/RingEigenvalue.lean consume.

theorem HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTGeneratorRecGamma0_succ_succ {N : ℕ} [NeZero N] {p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (hp : 0 < p) (hpN : p.Coprime N) (r : ℕ) : (heckeRingHomCuspCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 2)) = (heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p) * (heckeRingHomCuspCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 1)) - (↑(χ (ZMod.unitOfCoprime p hpN)) * ↑p ^ (k - 1)) • (heckeRingHomCuspCharSpace k χ) (heckeTGeneratorRecGamma0 N p r)

The recurrence on S_k(N, χ), as an equality of endomorphisms: T_{p^{r+2}} = Tₚ ∘ T_{p^{r+1}} − χ(p) p^{k−1} • T_{p^r} on the cusp-form character space. The modular statement transported along the inclusion of character spaces (cuspToModFormCharSpace_twistedHeckeSlashCuspFormCharLinearMap), which is injective.

theorem HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTGeneratorRecGamma0_succ_succ_apply {N : ℕ} [NeZero N] {p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (hp : 0 < p) (hpN : p.Coprime N) (F : ↥(cuspFormCharSpace k χ)) (r : ℕ) : ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 2))) F = ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) (((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorRecGamma0 N p (r + 1))) F) - (↑(χ (ZMod.unitOfCoprime p hpN)) * ↑p ^ (k - 1)) • ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorRecGamma0 N p r)) F

The recurrence at a cusp form: heckeRingHomCuspCharSpace_heckeTGeneratorRecGamma0_succ_succ evaluated. This is the pointwise interface, the shape the coefficient formulas of Prime/Power.lean and Newforms/RingEigenvalue.lean consume.