Index of Congruence Subgroups

Computes the index [SL₂(ℤ) : Γ₀(pᵏ)] = pᵏ⁻¹(p + 1) for prime p and k ≥ 1.

Main results

• Gamma0_prime_index : (Gamma0 p).index = p + 1 for prime p
• Gamma0_relindex_step : (Gamma0 (p^(k+1))).relIndex (Gamma0 (p^k)) = p
• Gamma0_prime_power_index : (Gamma0 (p^k)).index = p^(k-1) * (p + 1) for k ≥ 1

References

• Shimura, Theorem 3.24

theorem HeckeRing.GL2.Gamma0_prime_index (p : ℕ) (hp : Nat.Prime p) : (CongruenceSubgroup.Gamma0 p).index = p + 1

[SL₂(ℤ) : Γ₀(p)] = p + 1 for prime p.

theorem HeckeRing.GL2.Gamma0_relindex_step (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk : 0 < k) : (CongruenceSubgroup.Gamma0 (p ^ (k + 1))).relIndex (CongruenceSubgroup.Gamma0 (p ^ k)) = p

[Γ₀(pᵏ) : Γ₀(p^{k+1})] = p for k >= 1.

theorem HeckeRing.GL2.Gamma0_prime_power_index (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk : 0 < k) : (CongruenceSubgroup.Gamma0 (p ^ k)).index = p ^ (k - 1) * (p + 1)

[SL₂(ℤ) : Γ₀(pᵏ)] = p^(k-1) * (p + 1) for prime p and k >= 1.