GL₂ Hecke Algebra: Definitions for Theorem 3.24

Specialization of the GL_n Hecke algebra to n=2. Defines T(a,d), T(m), and structural lemmas for Shimura's Theorem 3.24.

Main definitions

• TAd -- T(a,d) basis element
• TPp -- scalar double coset T(p,p)
• TSum -- Shimura's T(m) = Σ T(a,d) over divisor pairs

References

• Shimura, Theorem 3.24

noncomputable def HeckeRing.GL2.TAd (a d : ℕ) : GLn.HeckeAlgebra 2

T(a,d) for n=2: the Hecke basis element for diagonal (a,d) with a | d. Returns 0 when a = 0 or d = 0 or a ∤ d.

Equations

• HeckeRing.GL2.TAd a d = if x : 0 < a ∧ 0 < d ∧ a ∣ d then HeckeRing.GLn.TElem ![a, d] else 0

theorem HeckeRing.GL2.T_ad_of_pos (a d : ℕ) (ha : 0 < a) (hd : 0 < d) (h : a ∣ d) : TAd a d = GLn.TElem ![a, d]

Unfold TAd to TElem when all positivity and divisibility conditions hold.

theorem HeckeRing.GL2.T_ad_eq_zero {a d : ℕ} (h : ¬(0 < a ∧ 0 < d ∧ a ∣ d)) : TAd a d = 0

TAd a d is zero when the positivity or divisibility conditions fail.

noncomputable def HeckeRing.GL2.TPp (p : ℕ) : GLn.HeckeAlgebra 2

T(p,p): the scalar double coset for prime p, equal to TAd p p.

Equations

• HeckeRing.GL2.TPp p = HeckeRing.GL2.TAd p p

theorem HeckeRing.GL2.T_pp_of_pos (p : ℕ) (hp : Nat.Prime p) : TPp p = GLn.TElem fun (x : Fin 2) => p

For p prime, T(p,p) equals the scalar diagonal element TElem(p,p).

theorem HeckeRing.GL2.T_pp_eq_T_ad (p : ℕ) : TPp p = TAd p p

T(p,p) is definitionally equal to TAd p p.

theorem HeckeRing.GL2.T_elem_ones_eq : (GLn.TElem fun (x : Fin 2) => 1) = 1

The all-ones diagonal element is the identity in the Hecke algebra.

@[simp]

theorem HeckeRing.GL2.T_ad_one_one : TAd 1 1 = 1

T(1,1) is the identity element.

noncomputable def HeckeRing.GL2.TSum (m : ℕ+) : GLn.HeckeAlgebra 2

T(m) = Σ_{a | m} T(a, m/a).

Equations

• HeckeRing.GL2.TSum m = ∑ a ∈ (↑m).divisors, HeckeRing.GL2.TAd a (↑m / a)

theorem HeckeRing.GL2.T_sum_prime (p : ℕ) (hp : Nat.Prime p) : TSum ⟨p, ⋯⟩ = TAd 1 p

For p prime, T(p) = TAd(1,p).

theorem HeckeRing.GL2.T_elem_mul_scalar (b : Fin 2 → ℕ) (hb_pos : ∀ (i : Fin 2), 0 < b i) (hb : GLn.DivChain 2 b) (c : ℕ) (hc : 0 < c) : (GLn.TElem b * GLn.TElem fun (x : Fin 2) => c) = GLn.TElem (b * fun (x : Fin 2) => c)

Multiplication by a scalar diagonal element: TElem(b) * TElem(c,c) = TElem(b * c).

theorem HeckeRing.GL2.T_pp_comm_T_elem (p : ℕ) (hp : Nat.Prime p) (a : Fin 2 → ℕ) (ha_pos : ∀ (i : Fin 2), 0 < a i) (ha : GLn.DivChain 2 a) : TPp p * GLn.TElem a = GLn.TElem a * TPp p

T(p,p) commutes with every diagonal element TElem(a) for p prime.

theorem HeckeRing.GL2.T_pp_pow (p : ℕ) (hp : Nat.Prime p) (i : ℕ) : TPp p ^ i = GLn.TElem fun (x : Fin 2) => p ^ i

T(p,p)^i = TElem(p^i, p^i): the i-th power of the scalar double coset.

theorem HeckeRing.GL2.T_sum_ppow_expansion (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : TSum ⟨p ^ k, ⋯⟩ = ∑ i ∈ Finset.range (k / 2 + 1), TAd (p ^ i) (p ^ (k - i))

Expand T(p^k) as a sum over divisor pairs with non-zero TAd terms.