Congruence subgroups

This defines congruence subgroups of SL(2, ℤ) such as Γ(N), Γ₀(N) and Γ₁(N) for N a natural number.

It also contains basic results about congruence subgroups.

Width of a subgroup

These results are in the Subgroup namespace to enable dot-notation, although they are specific to the case of subgroups of the modular group.

noncomputable def Subgroup.width (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : ℕ

The width of the cusp ∞ for a subgroup of SL(2, ℤ), i.e. the least n > 0 such that [1, n; 0, 1] ∈ Γ.

Equations

• Γ.width = Γ.relIndex (Subgroup.zpowers ModularGroup.T)

theorem Subgroup.width_ne_zero (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] : Γ.width ≠ 0

theorem Subgroup.T_pow_width_mem (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : ModularGroup.T ^ Γ.width ∈ Γ

theorem Subgroup.T_zpow_mem_iff (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) {n : ℤ} : ModularGroup.T ^ n ∈ Γ ↔ ↑Γ.width ∣ n

The integers n such that [1, n; 0, 1] ∈ Γ are precisely the multiples of Γ.width.

theorem Subgroup.T_pow_mem_iff (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (n : ℕ) : ModularGroup.T ^ n ∈ Γ ↔ Γ.width ∣ n

The integers n such that [1, n; 0, 1] ∈ Γ are precisely the multiples of Γ.width.

@[simp]

theorem Subgroup.Gamma_width (N : ℕ) : (CongruenceSubgroup.Gamma N).width = N

theorem Subgroup.ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) : ModularGroup.T ^ M ∈ CongruenceSubgroup.Gamma N.natAbs