# Documentation

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

# 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.

@[simp]
theorem SL_reduction_mod_hom_val (N : ) (γ : ) (i : Fin 2) (j : Fin 2) :
↑(↑() γ) i j = ↑(γ i j)
def Gamma (N : ) :

The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity modulo N.

Instances For
theorem Gamma_mem' (N : ) (γ : ) :
γ ↑() γ = 1
@[simp]
theorem Gamma_mem (N : ) (γ : ) :
γ ↑(γ 0 0) = 1 ↑(γ 0 1) = 0 ↑(γ 1 0) = 0 ↑(γ 1 1) = 1
theorem Gamma_normal (N : ) :
def Gamma0 (N : ) :

The congruence subgroup of SL(2, ℤ) of matrices whose lower left-hand entry reduces to zero modulo N.

Instances For
@[simp]
theorem Gamma0_mem (N : ) (A : ) :
A ↑(A 1 0) = 0
theorem Gamma0_det (N : ) (A : { x // x }) :
↑(Matrix.det A) = 1
def Gamma0Map (N : ) :
{ x // x } →* ZMod N

The group homomorphism from Gamma0 to ZMod N given by mapping a matrix to its lower right-hand entry.

Instances For
def Gamma1' (N : ) :
Subgroup { x // x }

The congruence subgroup Gamma1 (as a subgroup of Gamma0) of matrices whose bottom row is congruent to (0,1) modulo N.

Instances For
@[simp]
theorem Gamma1_mem' (N : ) (γ : { x // x }) :
γ ↑() γ = 1
theorem Gamma1_to_Gamma0_mem (N : ) (A : { x // x }) :
A ↑(A 0 0) = 1 ↑(A 1 1) = 1 ↑(A 1 0) = 0
def Gamma1 (N : ) :

The congruence subgroup Gamma1 of SL(2, ℤ) consisting of matrices whose bottom row is congruent to (0,1) modulo N.

Instances For
@[simp]
theorem Gamma1_mem (N : ) (A : ) :
A ↑(A 0 0) = 1 ↑(A 1 1) = 1 ↑(A 1 0) = 0
theorem Gamma1_in_Gamma0 (N : ) :

A congruence subgroup is a subgroup of SL(2, ℤ) which contains some Gamma N for some (N : ℕ+).

Instances For
theorem isCongruenceSubgroup_trans (H : ) (K : ) (h : H K) (h2 : ) :
theorem Gamma_cong_eq_self (N : ) (g : ) :
g =
theorem conj_cong_is_cong (g : ) (Γ : ) (h : ) :