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.

source

@[simp]

theorem SL_reduction_mod_hom_val (N : ℕ) (γ : matrix.special_linear_group (fin 2) ℤ) (i j : fin 2) :

↑(⇑(matrix.special_linear_group.map (int.cast_ring_hom (zmod N))) γ) i j = ↑(↑γ i j)

source

def Gamma (N : ℕ) :

subgroup (matrix.special_linear_group (fin 2) ℤ)

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

Equations

Gamma N = (matrix.special_linear_group.map (int.cast_ring_hom (zmod N))).ker

source

theorem Gamma_mem' (N : ℕ) (γ : matrix.special_linear_group (fin 2) ℤ) :

γ ∈ Gamma N ↔ ⇑(matrix.special_linear_group.map (int.cast_ring_hom (zmod N))) γ = 1

source

@[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

source

theorem Gamma_normal (N : ℕ) :

(Gamma N).normal

source

theorem Gamma_one_top :

Gamma 1 = ⊤

source

theorem Gamma_zero_bot :

Gamma 0 = ⊥

source

def Gamma0 (N : ℕ) :

subgroup (matrix.special_linear_group (fin 2) ℤ)

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

Equations

Gamma0 N = {carrier := {g : matrix.special_linear_group (fin 2) ℤ | ↑(↑g 1 0) = 0}, mul_mem' := _, one_mem' := _, inv_mem' := _}

source

@[simp]

theorem Gamma0_mem (N : ℕ) (A : matrix.special_linear_group (fin 2) ℤ) :

A ∈ Gamma0 N ↔ ↑(↑A 1 0) = 0

source

theorem Gamma0_det (N : ℕ) (A : ↥(Gamma0 N)) :

↑(A.val.val.det) = 1

source

def Gamma_0_map (N : ℕ) :

↥(Gamma0 N) →* zmod N

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

Equations

Gamma_0_map N = {to_fun := λ (g : ↥(Gamma0 N)), ↑(↑g 1 1), map_one' := _, map_mul' := _}

source

def Gamma1' (N : ℕ) :

subgroup ↥(Gamma0 N)

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

Equations

Gamma1' N = (Gamma_0_map N).ker

source

@[simp]

theorem Gamma1_mem' (N : ℕ) (γ : ↥(Gamma0 N)) :

γ ∈ Gamma1' N ↔ ⇑(Gamma_0_map N) γ = 1

source

theorem Gamma1_to_Gamma0_mem (N : ℕ) (A : ↥(Gamma0 N)) :

A ∈ Gamma1' N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

source

def Gamma1 (N : ℕ) :

subgroup (matrix.special_linear_group (fin 2) ℤ)

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

Equations

Gamma1 N = subgroup.map ((Gamma0 N).subtype.comp (Gamma1' N).subtype) ⊤

source

@[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

source

theorem Gamma1_in_Gamma0 (N : ℕ) :

Gamma1 N ≤ Gamma0 N

source

def is_congruence_subgroup (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) :

Prop

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

Equations

is_congruence_subgroup Γ = ∃ (N : ℕ+), Gamma ↑N ≤ Γ

source

theorem is_congruence_subgroup_trans (H K : subgroup (matrix.special_linear_group (fin 2) ℤ)) (h : H ≤ K) (h2 : is_congruence_subgroup H) :

is_congruence_subgroup K

source

theorem Gamma_is_cong_sub (N : ℕ+) :

is_congruence_subgroup (Gamma ↑N)

source

theorem Gamma1_is_congruence (N : ℕ+) :

is_congruence_subgroup (Gamma1 ↑N)

source

theorem Gamma0_is_congruence (N : ℕ+) :

is_congruence_subgroup (Gamma0 ↑N)

source

theorem Gamma_cong_eq_self (N : ℕ) (g : conj_act (matrix.special_linear_group (fin 2) ℤ)) :

g • Gamma N = Gamma N

source

theorem conj_cong_is_cong (g : conj_act (matrix.special_linear_group (fin 2) ℤ)) (Γ : subgroup (matrix.special_linear_group (fin 2) ℤ)) (h : is_congruence_subgroup Γ) :

is_congruence_subgroup (g • Γ)