The GL₂ multiplication table: telescoping identities

The first multiplication identity of Shimura's Theorem 3.24 for the GL₂ Hecke ring: T(1, pᵏ) = T(pᵏ) − T(p,p) · T(p^(k−2)) for k ≥ 2, by telescoping the divisor-pair expansion of T(pᵏ) against the index shift T(p,p) · T(pʲ, p^d) = T(p^(j+1), p^(d+1)).

The file also proves heckeT_prime_mul_heckeTDiag_one_prime_pow, Shimura's Theorem 3.24(5): T(p) · T(1, pᵏ) = T(1, p^(k+1)) + m · T(p, pᵏ), with multiplicity m = p + 1 at k = 1 and m = p otherwise. No positivity hypothesis on k is needed: at k = 0 the identity reads T(p) = T(1, p), since T(1,1) = 1 and T(p,1) = 0 for prime p.

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

Main results

• HeckeRing.GL2.heckeTDiag_one_prime_pow_eq: T(1, pᵏ) = T(pᵏ) − T(p,p) · T(p^(k−2)).

References

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

@[simp]

theorem HeckeRing.GL2.heckeTScalar_mul_heckeTDiag (c a d : ℕ) : heckeTScalar c * heckeTDiag a d = heckeTDiag (c * a) (c * d)

Scaling a diagonal Hecke element: T(c,c) · T(a,d) = T(c·a, c·d), with no hypotheses.

heckeTDiag is zero-extended off the divisor-pair range, and that extension is compatible with scaling: outside the range both sides vanish, since 0 < c·a forces 0 < a, and for 0 < c the divisibility c·a ∣ c·d is equivalent to a ∣ d. Primality plays no role, and neither does the shape of a and d.

theorem HeckeRing.GL2.heckeTScalar_mul_heckeTDiag_prime_pow (p j d : ℕ) : heckeTScalar p * heckeTDiag (p ^ j) (p ^ d) = heckeTDiag (p ^ (j + 1)) (p ^ (d + 1))

The index shift: T(p,p) · T(pʲ, p^d) = T(p^(j+1), p^(d+1)), for arbitrary p, j, d.

The prime-power case of heckeTScalar_mul_heckeTDiag; like it, unconditional.

Deliberately not @[simp]: the general rule carries the attribute, and it already rewrites this left-hand side (to T(p·pʲ, p·p^d)), so annotating the specialisation too would leave its left-hand side outside simp normal form — simpNF rejects exactly that. Callers wanting the p^(j+1) form rewrite with this lemma by name.

theorem HeckeRing.GL2.heckeTDiag_one_prime_pow_eq (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk : 2 ≤ k) : heckeTDiag 1 (p ^ k) = heckeT ⟨p ^ k, ⋯⟩ - heckeTScalar p * heckeT ⟨p ^ (k - 2), ⋯⟩

Shimura, Theorem 3.24(2): T(1, pᵏ) = T(pᵏ) − T(p,p) · T(p^(k−2)) for k ≥ 2: the divisor-pair expansion of T(pᵏ) telescopes against the index shift.

Support analysis for T(1,p) · T(1,pᵏ)

Every double coset in the support of the product T(1,p) · T(1,pᵏ) is T(1, p^(k+1)) or T(p, pᵏ): the determinant balances to p^(k+1), and the first invariant factor divides p because the conjugated middle matrix stays integral.

theorem HeckeRing.GL2.heckeT_prime_mul_heckeTDiag_one_prime_pow (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : heckeT ⟨p, ⋯⟩ * heckeTDiag 1 (p ^ k) = heckeTDiag 1 (p ^ (k + 1)) + (if k = 1 then ↑p + 1 else ↑p) • heckeTDiag p (p ^ k)

Shimura, Theorem 3.24(5): T(p) · T(1, pᵏ) = T(1, p^(k+1)) + m · T(p, pᵏ), where the multiplicity m is p + 1 for k = 1 and p for k ≥ 2.

@[simp]

theorem HeckeRing.GL2.heckeTDiag_one_prime_mul_heckeTDiag_one_prime_pow (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : heckeTDiag 1 p * heckeTDiag 1 (p ^ k) = heckeTDiag 1 (p ^ (k + 1)) + (if k = 1 then ↑p + 1 else ↑p) • heckeTDiag p (p ^ k)

The characteristic product rule in simp normal form: T(1, p) · T(1, pᵏ) = T(1, p^(k+1)) + m · T(p, pᵏ).

heckeT_prime_mul_heckeTDiag_one_prime_pow states the same identity with T(p) on the left, but @[simp] heckeT_prime rewrites that T(p) to T(1, p) first, so the rule can never fire during simplification. This restatement is the form simp actually meets, and carries the attribute.