The degree of a rank-two diagonal double coset

The degree of a double coset is the relative index of the conjugated copy of SL₂(ℤ). For a diagonal representative a = (a₀, a₁) with a₀ ∣ a₁ whose ratio N = a₁ / a₀ is positive, conjugating SL₂(ℤ) by natDiagGL 2 a carves out exactly Γ₀(N), so

deg T(a₀, a₁) = [SL₂(ℤ) : Γ₀(N)],

and specializing to N = pᵏ with the index computed in TauCeti.NumberTheory.ModularForms.CongruenceSubgroups.Basic gives Shimura's pᵏ⁻¹(p + 1).

Positivity of the ratio is needed: it forces both entries positive, and so rules out the tuples on which natDiagGL takes its junk value 1 (for a = (0, 0) the ratio is 0).

Note that the degree is not the number of diagonal representatives: for a = (1, p) that count is p, while the true degree is p + 1 — the double coset also contains representatives with permuted diagonals.

Main results

• degree_diagCoset_eq_Gamma0_index: deg T(a₀, a₁) = [SL₂(ℤ) : Γ₀(N)] for a divisibility chain a whose ratio N = a₁ / a₀ is positive.
• degree_diagCoset_of_ratio_eq_prime_pow: deg T(a₀, a₁) = pᵏ⁻¹(p + 1) for a divisibility chain a whose ratio is pᵏ, with p prime and k ≥ 1.

The rank-general constant case deg T(c, ..., c) = 1 is in TauCeti/NumberTheory/HeckeRing/GLn/Degree.lean.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/Degree.lean, Chris Birkbeck), split out of the rank-general material of that file, since the Γ₀-index computation is specific to rank two.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Propositions 3.14, 3.18 and Theorem 3.24.

theorem HeckeRing.GL2.degree_diagCoset_eq_Gamma0_index (N : ℕ) (hN : 0 < N) (a : Fin 2 → ℕ) (hdiv : GLn.IsDvdChain a) (h_ratio : a 1 / a 0 = N) : (GLn.diagCoset a).degree = (CongruenceSubgroup.Gamma0 N).index

The degree of a rank-two diagonal double coset is an index of Γ₀: if a is a divisibility chain whose entries are in ratio N > 0, then deg T(a₀, a₁) = [SL₂(ℤ) : Γ₀(N)]. Conjugating SL₂(ℤ) by the diagonal matrix a carves out exactly Γ₀(N), so the relative index computing the degree is the index of Γ₀(N).

theorem HeckeRing.GL2.degree_diagCoset_of_ratio_eq_prime_pow (p : ℕ) (hp : Nat.Prime p) (a : Fin 2 → ℕ) (hdiv : GLn.IsDvdChain a) (k : ℕ) (hk : 0 < k) (h_ratio : a 1 / a 0 = p ^ k) : (GLn.diagCoset a).degree = p ^ (k - 1) * (p + 1)

The prime-power degree (Shimura, Theorem 3.24, degree count): for prime p and k ≥ 1, a divisibility chain a of ratio a₁ / a₀ = pᵏ has deg T(a₀, a₁) = pᵏ⁻¹ (p + 1). The archetype is a = (pⁱ, pⁱ⁺ᵏ).