Shimura Theorem 3.24: Multiplication Table for GL₂ Hecke Algebra

The multiplication identities for the n=2 Hecke algebra (identities 1--5). Degree formulas (identities 6--7) are in GL2.Degree.

Main results

• T_ad_one_ppow_eq — T(1,pᵏ) = T(pᵏ) − T(p,p) · T(p^{k−2}) for k ≥ 2
• T_sum_mul — T(m) · T(n) = Σ d · T(d,d) · T(mn/d²)
• T_sum_ppow_mul — T(pʳ) · T(pˢ) = Σ pⁱ · T(pⁱ,pⁱ) · T(p^{r+s−2i}) for r ≤ s
• T_sum_prime_mul_T_ad — T(p) · T(1,pᵏ) = T(1,p^{k+1}) + m · T(p,pᵏ) (key computation)

References

• Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Theorem 3.24

theorem HeckeRing.GL2.SLnZ_to_GLnQ_det {n : ℕ} [NeZero n] (S : Matrix.SpecialLinearGroup (Fin n) ℤ) : (↑((Matrix.SpecialLinearGroup.mapGL ℚ) S)).det = 1

SL_n(ℤ) → GL_n(ℚ) has determinant 1 (replaces removed SLnZ_to_GLnQ_det).

theorem HeckeRing.GL2.SLnZ_to_GLnQ_val {n : ℕ} [NeZero n] (S : Matrix.SpecialLinearGroup (Fin n) ℤ) : ↑((Matrix.SpecialLinearGroup.mapGL ℚ) S) = (↑S).map ⇑(algebraMap ℤ ℚ)

SL_n(ℤ) → GL_n(ℚ) coercion as a matrix (replaces removed SLnZ_to_GLnQ_val).

Ring algebra lemmas for HeckeAlgebra 2

In mathlib v4.29, rw [mul_sub] etc. fail on HeckeAlgebra 2 because the Mul instance from instMul𝕋Int (the custom Hecke multiplication) is not definitionally equal to the Mul carried by NonUnitalNonAssocRing.toDistrib.toMul inside mul_sub. These local lemmas provide the ring identities with the correct Mul instance.

Identity 1: T(m) = Σ T(a,d) — definitional

Shimura's T(m) is defined as TSum m, which is exactly the sum Σ_{a ∣ m, a²∣m} T(a, m/a). This identity is the definition itself.

Identity 2: Telescoping

theorem HeckeRing.GL2.T_ad_one_ppow_eq (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk : 2 ≤ k) : TAd 1 (p ^ k) = TSum ⟨p ^ k, ⋯⟩ - TPp p * TSum ⟨p ^ (k - 2), ⋯⟩

Theorem 3.24(2): T(1, pᵏ) = T(pᵏ) − T(p,p) · T(p^{k−2}) for k ≥ 2. Proof strategy: T(pᵏ) = Σ T(pⁱ,p^{k-i}) and T(p,p)·T(p^{k-2}) shifts the index, giving a telescoping cancellation.

Identity 5: The key recursion

theorem HeckeRing.GL2.matrix_isolate_middle (L_ℤ M R_ℤ D : Matrix (Fin 2) (Fin 2) ℤ) (hLadj : L_ℤ.adjugate * L_ℤ = 1) (hRadj : R_ℤ * R_ℤ.adjugate = 1) (heq_LMR : L_ℤ * M * R_ℤ = D) : M = L_ℤ.adjugate * D * R_ℤ.adjugate

If L * M * R = D with L, R having determinant 1, then M = L.adj * D * R.adj.

theorem HeckeRing.GL2.T_sum_prime_mul_T_ad (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk : 0 < k) : TSum ⟨p, ⋯⟩ * TAd 1 (p ^ k) = TAd 1 (p ^ (k + 1)) + (if k = 1 then ↑(p + 1) else ↑p) • TAd p (p ^ k)

Theorem 3.24(5): T(p) · T(1, pᵏ) = T(1, p^{k+1}) + m · T(p, pᵏ)

theorem HeckeRing.GL2.T_sum_one : TSum 1 = 1

TSum(1) = 1: the sum over divisor pairs of 1 is the identity.

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

Theorem 3.24(6 recurrence): T(p^{k+1}) = T(p) T(p^k) - p T(p,p) T(p^{k-1}) for k >= 1.

Identity 4: General prime-power product

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

Theorem 3.24(4): T(p^r) T(p^s) = sum_{i=0}^{r} p^i T(p^i,p^i) T(p^{r+s-2i}) for r <= s.

Identity 3: General multiplicativity

theorem HeckeRing.GL2.T_ad_mul_of_coprime (a b da db : ℕ) (ha : 0 < a) (hb : 0 < b) (hda : 0 < da) (hdb : 0 < db) (hdva : a ∣ da) (hdvb : b ∣ db) (hcop : (a * da).Coprime (b * db)) : TAd a da * TAd b db = TAd (a * b) (da * db)

Coprime factoring: T(a,da) T(b,db) = T(ab,da*db) when a*da and b*db are coprime.

theorem HeckeRing.GL2.mul_injOn_coprime_divisors (m n : ℕ) (hcop : m.Coprime n) : Set.InjOn (fun (p : ℕ × ℕ) => p.1 * p.2) ↑(m.divisors ×ˢ n.divisors)

The multiplication map on m.divisors ×ˢ n.divisors is injective when m and n are coprime.

theorem HeckeRing.GL2.T_sum_mul_coprime (m n : ℕ+) (hcop : (↑m).Coprime ↑n) : TSum m * TSum n = TSum ⟨↑m * ↑n, ⋯⟩

Theorem 3.24(3a): coprime multiplicativity T(m) T(n) = T(mn) when gcd(m,n) = 1.

noncomputable def HeckeRing.GL2.TSumNat (k : ℕ) : GLn.HeckeAlgebra 2

TSum extended to ℕ: agrees with TSum for positive arguments, zero for 0.

Equations

• HeckeRing.GL2.TSumNat k = ∑ a ∈ k.divisors, HeckeRing.GL2.TAd a (k / a)

theorem HeckeRing.GL2.T_sum_nat_eq (k : ℕ+) : TSumNat ↑k = TSum k

TSumNat agrees with TSum on positive naturals.

theorem HeckeRing.GL2.gcd_pow_pow_of_le (q r s : ℕ) (hrs : r ≤ s) : (q ^ r).gcd (q ^ s) = q ^ r

gcd(q^r, q^s) = q^r when r <= s.

theorem HeckeRing.GL2.gcd_factor_prime_pow (q : ℕ) (hq : Nat.Prime q) (a b : ℕ) (m' n' : ℕ+) (hqm : ¬q ∣ ↑m') (hqn : ¬q ∣ ↑n') : (q ^ a * ↑m').gcd (q ^ b * ↑n') = q ^ min a b * (↑m').gcd ↑n'

GCD factoring: gcd(q^a * m', q^b * n') = q^(min a b) * gcd(m', n').

theorem HeckeRing.GL2.T_sum_mul (m n : ℕ+) : TSum m * TSum n = ∑ d ∈ ((↑m).gcd ↑n).divisors, ↑d • (TAd d d * TSumNat (↑m * ↑n / (d * d)))

Theorem 3.24(3): T(m) · T(n) = Σ_{d∣gcd(m,n)} d · T(d,d) · T(mn/d²). From Identity 4 at each prime + coprime multiplicativity.