# mathlib3documentation

number_theory.modular_forms.congruence_subgroups

# Congruence subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Equations
theorem Gamma_mem' (N : ) (γ : ) :
γ
@[simp]
theorem Gamma_mem (N : ) (γ : ) :
γ (γ 0 0) = 1 (γ 0 1) = 0 (γ 1 0) = 0 (γ 1 1) = 1
theorem Gamma_normal (N : ) :
theorem Gamma_one_top  :
theorem Gamma_zero_bot  :
def Gamma0 (N : ) :

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

Equations
@[simp]
theorem Gamma0_mem (N : ) (A : ) :
A (A 1 0) = 0
theorem Gamma0_det (N : ) (A : (Gamma0 N)) :
(A.val.val.det) = 1
def Gamma_0_map (N : ) :

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

Equations
def Gamma1' (N : ) :

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

Equations
@[simp]
theorem Gamma1_mem' (N : ) (γ : (Gamma0 N)) :
γ (Gamma_0_map N) γ = 1
theorem Gamma1_to_Gamma0_mem (N : ) (A : (Gamma0 N)) :
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.

Equations
@[simp]
theorem Gamma1_mem (N : ) (A : ) :
A (A 0 0) = 1 (A 1 1) = 1 (A 1 0) = 0
theorem Gamma1_in_Gamma0 (N : ) :
def is_congruence_subgroup (Γ : subgroup ) :
Prop

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

Equations
theorem is_congruence_subgroup_trans (H K : subgroup ) (h : H K) (h2 : is_congruence_subgroup H) :
theorem Gamma_is_cong_sub (N : ℕ+) :
theorem Gamma1_is_congruence (N : ℕ+) :
theorem Gamma0_is_congruence (N : ℕ+) :
theorem Gamma_cong_eq_self (N : ) (g : conj_act ) :
g =