The GL₂ multiplication table: the prime-power recurrence

Shimura's Theorem 3.24(4): the summed Hecke operators at a prime satisfy

T(p^(k+1)) = T(p) · T(pᵏ) − p · T(p,p) · T(p^(k−1)) for k ≥ 1,

which determines every T(pᵏ) from T(p) and the scalar operator. The proof feeds the key product identity T(p) · T(1,pᵏ) = T(1,p^(k+1)) + m · T(p,pᵏ) into the telescoping identity T(1,pᵏ) = T(pᵏ) − T(p,p) · T(p^(k−2)), by strong induction on k.

The recurrence then yields the full product formula T(pʳ) · T(pˢ) = ∑_{i ≤ r} pⁱ · T(p,p)ⁱ · T(p^(r+s−2i)) for r ≤ s, again by strong induction: each summand splits in two through the recurrence, and the scalar operator is central, so the shifted copy cancels against the subtracted term.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/MultiplicationTable.lean, Chris Birkbeck), recurrence section.

Main results

• HeckeRing.GL2.heckeTDiag_p_prime_pow_eq: T(p, pᵏ) = T(p,p) · T(1, p^(k−1)).
• HeckeRing.GL2.heckeT_prime_pow_recurrence: the prime-power recurrence.
• HeckeRing.GL2.heckeT_prime_pow_mul: the product formula T(pʳ) · T(pˢ) = ∑_{i ≤ r} pⁱ · T(p,p)ⁱ · T(p^(r+s−2i)) for r ≤ s.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Theorem 3.24.

theorem HeckeRing.GL2.heckeTDiag_p_prime_pow_eq (p k : ℕ) (hk : 0 < k) : heckeTDiag p (p ^ k) = heckeTScalar p * heckeTDiag 1 (p ^ (k - 1))

T(p, pᵏ) = T(p,p) · T(1, p^(k−1)) for k ≥ 1: the index shift at the bottom of the divisor pair.

Like the index shift it specializes, this is unconditional: heckeTDiag is zero-extended, so no positivity or primality hypothesis is needed.

theorem HeckeRing.GL2.heckeT_prime_pow_recurrence (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : 0 < k → heckeT ⟨p ^ (k + 1), ⋯⟩ = heckeT ⟨p, ⋯⟩ * heckeT ⟨p ^ k, ⋯⟩ - ↑p • (heckeTScalar p * heckeT ⟨p ^ (k - 1), ⋯⟩)

Shimura, Theorem 3.24(4) — the prime-power recurrence: T(p^(k+1)) = T(p) · T(pᵏ) − p · T(p,p) · T(p^(k−1)) for k ≥ 1, which determines every T(pᵏ) from T(p) and the scalar operator.

The product formula

r ↦ T(pʳ) is a second-order linear recurrence: heckeT_prime_pow_recurrence says it obeys d (r + 2) = D * d (r + 1) - S * d r with D = T(p) and S = p • T(p,p). The product formula is therefore an instance of TauCeti.linearRec₂_mul_eq_sum_pow_mul, which holds for any such sequence over any ring in which D and S commute — and here they do, the scalar operator being central.

theorem HeckeRing.GL2.heckeT_prime_pow_mul (p : ℕ) (hp : Nat.Prime p) (r s : ℕ) : r ≤ s → heckeT ⟨p ^ r, ⋯⟩ * heckeT ⟨p ^ s, ⋯⟩ = ∑ i ∈ Finset.range (r + 1), ↑p ^ i • (heckeTScalar p ^ i * heckeT ⟨p ^ (r + s - 2 * i), ⋯⟩)

Shimura, Theorem 3.24(4) — the prime-power product formula: T(pʳ) · T(pˢ) = ∑_{i ≤ r} pⁱ · T(p,p)ⁱ · T(p^(r+s−2i)) for r ≤ s.

This is TauCeti.linearRec₂_mul_eq_sum_pow_mul at d = fun r ↦ T(pʳ), D = T(p) and S = p • T(p,p); all that is left is to match the summand, since the general statement writes S ^ i * _ where this one writes pⁱ • (T(p,p)ⁱ * _).