Degrees of the GL₂ Hecke operators

Shimura's Theorem 3.24, identities (6) and (7): the double coset of diag(pⁱ, pⁱ⁺ᵏ) has degree pᵏ⁻¹(p + 1) for k > 0, and the degrees of the summed operators T(m) assemble into the divisor-sum function, deg T(m) = σ₁(m).

The prime-power case is a two-step induction on k. Expanding T(pᵏ) into its diagonal terms T(pⁱ, pᵏ⁻ⁱ), raising k by two shifts the indexing by one place and leaves every term's degree unchanged, so only the new leading term T(1, pᵏ⁺²) contributes and deg T(pᵏ⁺²) = deg T(pᵏ) + pᵏ⁺¹(p + 1). Multiplicativity of T in coprime arguments then upgrades the prime-power formula to every m.

Main results

• HeckeRing.GL2.degree_diagCoset_prime_pow: deg T(pⁱ, pⁱ⁺ᵏ) = pᵏ⁻¹(p + 1) for k > 0.
• HeckeRing.GL2.deg_heckeT_prime_pow: deg T(pᵏ) = 1 + p + ⋯ + pᵏ.
• HeckeRing.GL2.deg_heckeT: deg T(m) = σ₁(m).

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Degree.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms).

References

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

theorem HeckeRing.GL2.degree_diagCoset_prime_pow (p : ℕ) (hp : Nat.Prime p) (i k : ℕ) (hk : 0 < k) : (GLn.diagCoset ![p ^ i, p ^ (i + k)]).degree = p ^ (k - 1) * (p + 1)

The prime-power coset degree (Shimura, Theorem 3.24(6)): deg T(pⁱ, pⁱ⁺ᵏ) = pᵏ⁻¹(p + 1) for k > 0.

theorem HeckeRing.GL2.deg_heckeT_prime_pow (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : (LeftCosetModule.deg (GLn.posDetInt 2) (GLn.SLnZ 2) ℤ) (heckeT ⟨p ^ k, ⋯⟩) = ∑ j ∈ Finset.range (k + 1), ↑p ^ j

The prime-power degree (Shimura, Theorem 3.24(7) at a prime power): deg T(pᵏ) = 1 + p + ⋯ + pᵏ.

@[simp]

theorem HeckeRing.GL2.deg_heckeT (m : ℕ+) : (LeftCosetModule.deg (GLn.posDetInt 2) (GLn.SLnZ 2) ℤ) (heckeT m) = ↑((ArithmeticFunction.sigma 1) ↑m)

The degree of T(m) (Shimura, Theorem 3.24(7)): deg T(m) = σ₁(m).