The cusps of Γ₀(N)

The number of cusps of Γ₀(N) is ε∞ = ∑_{g ∣ N} φ(gcd(g, N / g)), the cusp count in the dimension formulas for Γ₀(N). Cusps are counted as the cusp orbits of the effective image of Γ₀(N) in PSL(2, ℝ), the boundary orbits adjoined to its analytic quotient.

Every cusp is γ • ∞ for some γ ∈ SL(2, ℤ). For γ and γ' with bottom rows (c, d) and (c', d'), the cusps γ • ∞ and γ' • ∞ are Γ₀(N)-equivalent exactly when N ∣ c d' - c' d + j c c' for some integer j. This congruence is detected by the label of γ: the divisor g = gcd(c, N) of N, together with the residue of (c / g) / d modulo gcd(g, N / g), which is a unit. Every divisor and every unit residue occur, so the cusps of Γ₀(N) are in bijection with the pairs (g, x) with g ∣ N and x ∈ (ℤ / gcd(g, N / g))ˣ.

Main definitions

• TauCeti.gamma0CuspLabel: the label (g, x) of γ ∈ SL(2, ℤ).
• TauCeti.gamma0CuspOrbitEquiv: the cusp orbits of Γ₀(N) are in bijection with the labels.

Main results

• TauCeti.cuspOrbitOfSL2Z_Gamma0_eq_iff: the congruence criterion for equivalence of cusps.
• TauCeti.gamma0CuspLabel_eq_iff: two matrices have the same label exactly when they represent the same cusp.
• TauCeti.card_cuspOrbit_Gamma0: the cusp count ε∞ = ∑_{g ∣ N} φ(gcd(g, N / g)).
• TauCeti.card_cuspOrbit_Gamma0_of_prime: Γ₀(p) has two cusps.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §3.8.
• G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §1.6, Proposition 1.43.

Equivalence of cusps

theorem TauCeti.cuspOrbitOfSL2Z_Gamma0_eq_iff {N : ℕ} [NeZero N] (γ γ' : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (CongruenceSubgroup.Gamma0 N).cuspOrbitOfSL2Z γ = (CongruenceSubgroup.Gamma0 N).cuspOrbitOfSL2Z γ' ↔ ∃ (j : ℤ), ↑N ∣ ↑γ 1 0 * ↑γ' 1 1 - ↑γ' 1 0 * ↑γ 1 1 + j * ↑γ 1 0 * ↑γ' 1 0

The criterion for equivalence of cusps of Γ₀(N). For γ and γ' with bottom rows (c, d) and (c', d'), the cusps γ • ∞ and γ' • ∞ are Γ₀(N)-equivalent exactly when N ∣ c d' - c' d + j c c' for some integer j.

Labels of cusps

noncomputable def TauCeti.gamma0CuspLabel (N : ℕ) [NeZero N] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (g : ↥N.divisors) × (ZMod ((↑g).gcd (N / ↑g)))ˣ

The label of the cusp γ • ∞ of Γ₀(N). For γ ∈ SL(2, ℤ) with bottom row (c, d), it is the divisor g = gcd(c, N) of N together with the unit (c / g) / d modulo gcd(g, N / g). Matrices representing the same cusp have the same label (gamma0CuspLabel_eq_iff), and gamma0CuspOrbitEquiv is the resulting bijection.

@[simp]

theorem TauCeti.coe_gamma0CuspLabel_fst {N : ℕ} [NeZero N] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(gamma0CuspLabel N γ).fst = (↑γ 1 0).gcd ↑N

The divisor in the label of γ is gcd(c, N), for c the lower-left entry of γ.

theorem TauCeti.coe_gamma0CuspLabel_snd_mul {N : ℕ} [NeZero N] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(gamma0CuspLabel N γ).snd * ↑(↑γ 1 1) = ↑(↑γ 1 0 / ↑((↑γ 1 0).gcd ↑N))

The residue in the label of γ is (c / g) / d, for (c, d) the bottom row of γ and g = gcd(c, N): its product with d is c / g.

theorem TauCeti.gamma0CuspLabel_eq_iff_exists_dvd {N : ℕ} [NeZero N] (γ γ' : Matrix.SpecialLinearGroup (Fin 2) ℤ) : gamma0CuspLabel N γ = gamma0CuspLabel N γ' ↔ ∃ (j : ℤ), ↑N ∣ ↑γ 1 0 * ↑γ' 1 1 - ↑γ' 1 0 * ↑γ 1 1 + j * ↑γ 1 0 * ↑γ' 1 0

Two matrices have the same label exactly when their bottom rows (c, d) and (c', d') satisfy N ∣ c d' - c' d + j c c' for some integer j.

theorem TauCeti.gamma0CuspLabel_eq_iff_gcd_eq_of_squarefree {N : ℕ} [NeZero N] (hN : Squarefree N) (γ γ' : Matrix.SpecialLinearGroup (Fin 2) ℤ) : gamma0CuspLabel N γ = gamma0CuspLabel N γ' ↔ (↑γ 1 0).gcd ↑N = (↑γ' 1 0).gcd ↑N

At squarefree level, two cusp labels agree exactly when their denominator gcds agree.

theorem TauCeti.gamma0CuspLabel_surjective {N : ℕ} [NeZero N] : Function.Surjective (gamma0CuspLabel N)

Every divisor g of N and every unit modulo gcd(g, N / g) is a label: that of a matrix with bottom row (g, d).

theorem TauCeti.gamma0CuspLabel_eq_iff {N : ℕ} [NeZero N] (γ γ' : Matrix.SpecialLinearGroup (Fin 2) ℤ) : gamma0CuspLabel N γ = gamma0CuspLabel N γ' ↔ (CongruenceSubgroup.Gamma0 N).cuspOrbitOfSL2Z γ = (CongruenceSubgroup.Gamma0 N).cuspOrbitOfSL2Z γ'

Two matrices have the same label exactly when they represent the same cusp of Γ₀(N).

noncomputable def TauCeti.gamma0CuspOrbitEquiv (N : ℕ) [NeZero N] : (Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma0 N)).CuspOrbit ≃ (g : ↥N.divisors) × (ZMod ((↑g).gcd (N / ↑g)))ˣ

The cusps of Γ₀(N) are in bijection with the pairs (g, x) of a divisor g of N and a unit x modulo gcd(g, N / g). The cusp γ • ∞ corresponds to the label of γ (gamma0CuspOrbitEquiv_cuspOrbitOfSL2Z).

@[simp]

theorem TauCeti.gamma0CuspOrbitEquiv_cuspOrbitOfSL2Z {N : ℕ} [NeZero N] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (gamma0CuspOrbitEquiv N) ((CongruenceSubgroup.Gamma0 N).cuspOrbitOfSL2Z γ) = gamma0CuspLabel N γ

The cusp γ • ∞ of Γ₀(N) corresponds to the label of γ.

@[simp]

theorem TauCeti.gamma0CuspOrbitEquiv_symm_gamma0CuspLabel {N : ℕ} [NeZero N] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (gamma0CuspOrbitEquiv N).symm (gamma0CuspLabel N γ) = (CongruenceSubgroup.Gamma0 N).cuspOrbitOfSL2Z γ

The cusp with the label of γ is γ • ∞.

theorem TauCeti.card_cuspOrbit_Gamma0 (N : ℕ) [NeZero N] : Nat.card (Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma0 N)).CuspOrbit = ∑ g ∈ N.divisors, (g.gcd (N / g)).totient

The cusp count ε∞ of Γ₀(N): the number of cusps of Γ₀(N) is ∑_{g ∣ N} φ(gcd(g, N / g)).

theorem TauCeti.card_cuspOrbit_Gamma0_of_prime {p : ℕ} [Fact (Nat.Prime p)] : Nat.card (Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma0 p)).CuspOrbit = 2

Γ₀(p) has two cusps for a prime p.