mathlib3 documentation

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.

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

Equations
@[simp]
theorem Gamma_mem (N : ) (γ : matrix.special_linear_group (fin 2) ) :
γ Gamma 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  :

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 : matrix.special_linear_group (fin 2) ) :
A Gamma0 N (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)) :
theorem Gamma1_to_Gamma0_mem (N : ) (A : (Gamma0 N)) :
A Gamma1' N (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
@[simp]
theorem Gamma1_mem (N : ) (A : matrix.special_linear_group (fin 2) ) :
A Gamma1 N (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 : ℕ+).

Equations