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

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

Equations
Instances For
theorem CongruenceSubgroup.Gamma_mem' (N : ) (γ : ) :
= 1
@[simp]
theorem CongruenceSubgroup.Gamma_mem (N : ) (γ : ) :
(γ 0 0) = 1 (γ 0 1) = 0 (γ 1 0) = 0 (γ 1 1) = 1

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

Equations
• = { carrier := {g : | (g 1 0) = 0}, mul_mem' := , one_mem' := , inv_mem' := }
Instances For
@[simp]
theorem CongruenceSubgroup.Gamma0_mem (N : ) (A : ) :
(A 1 0) = 0
theorem CongruenceSubgroup.Gamma0_det (N : ) (A : ) :
(A).det = 1

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

Equations
• = { toFun := fun (g : ) => (g 1 1), map_one' := , map_mul' := }
Instances For

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

Equations
Instances For
@[simp]
theorem CongruenceSubgroup.Gamma1_mem' (N : ) (γ : ) :
theorem CongruenceSubgroup.Gamma1_to_Gamma0_mem (N : ) (A : ) :
(A 0 0) = 1 (A 1 1) = 1 (A 1 0) = 0

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

Equations
Instances For
@[simp]
theorem CongruenceSubgroup.Gamma1_mem (N : ) (A : ) :
(A 0 0) = 1 (A 1 1) = 1 (A 1 0) = 0

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

Equations
Instances For