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 : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (i : Fin 2) (j : Fin 2) : ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑(↑γ i j)

def CongruenceSubgroup.Gamma (N : ℕ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

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

Equations

• CongruenceSubgroup.Gamma N = (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))).ker

theorem CongruenceSubgroup.Gamma_mem' (N : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ CongruenceSubgroup.Gamma N ↔ (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1

@[simp]

theorem CongruenceSubgroup.Gamma_mem (N : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : γ ∈ CongruenceSubgroup.Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1

theorem CongruenceSubgroup.Gamma_normal (N : ℕ) : (CongruenceSubgroup.Gamma N).Normal

theorem CongruenceSubgroup.Gamma_one_top : CongruenceSubgroup.Gamma 1 = ⊤

theorem CongruenceSubgroup.Gamma_zero_bot : CongruenceSubgroup.Gamma 0 = ⊥

theorem CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma (N : ℤ) (M : ℤ) (hNM : N ∣ M) : ModularGroup.T ^ M ∈ CongruenceSubgroup.Gamma N.natAbs

def CongruenceSubgroup.Gamma0 (N : ℕ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

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

Equations

• CongruenceSubgroup.Gamma0 N = { carrier := {g : Matrix.SpecialLinearGroup (Fin 2) ℤ | ↑(↑g 1 0) = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem CongruenceSubgroup.Gamma0_mem (N : ℕ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : A ∈ CongruenceSubgroup.Gamma0 N ↔ ↑(↑A 1 0) = 0

theorem CongruenceSubgroup.Gamma0_det (N : ℕ) (A : ↥(CongruenceSubgroup.Gamma0 N)) : ↑(↑↑A).det = 1

def CongruenceSubgroup.Gamma0Map (N : ℕ) : ↥(CongruenceSubgroup.Gamma0 N) →* ZMod N

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

Equations

• CongruenceSubgroup.Gamma0Map N = { toFun := fun (g : ↥(CongruenceSubgroup.Gamma0 N)) => ↑(↑↑g 1 1), map_one' := ⋯, map_mul' := ⋯ }

def CongruenceSubgroup.Gamma1' (N : ℕ) : Subgroup ↥(CongruenceSubgroup.Gamma0 N)

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

Equations

• CongruenceSubgroup.Gamma1' N = (CongruenceSubgroup.Gamma0Map N).ker

@[simp]

theorem CongruenceSubgroup.Gamma1_mem' (N : ℕ) (γ : ↥(CongruenceSubgroup.Gamma0 N)) : γ ∈ CongruenceSubgroup.Gamma1' N ↔ (CongruenceSubgroup.Gamma0Map N) γ = 1

theorem CongruenceSubgroup.Gamma1_to_Gamma0_mem (N : ℕ) (A : ↥(CongruenceSubgroup.Gamma0 N)) : A ∈ CongruenceSubgroup.Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

def CongruenceSubgroup.Gamma1 (N : ℕ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

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

Equations

• CongruenceSubgroup.Gamma1 N = Subgroup.map ((CongruenceSubgroup.Gamma0 N).subtype.comp (CongruenceSubgroup.Gamma1' N).subtype) ⊤

@[simp]

theorem CongruenceSubgroup.Gamma1_mem (N : ℕ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) : A ∈ CongruenceSubgroup.Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0

theorem CongruenceSubgroup.Gamma1_in_Gamma0 (N : ℕ) : CongruenceSubgroup.Gamma1 N ≤ CongruenceSubgroup.Gamma0 N

def CongruenceSubgroup.IsCongruenceSubgroup (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Prop

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

Equations

• CongruenceSubgroup.IsCongruenceSubgroup Γ = ∃ (N : ℕ+), CongruenceSubgroup.Gamma ↑N ≤ Γ

theorem CongruenceSubgroup.isCongruenceSubgroup_trans (H : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (K : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (h : H ≤ K) (h2 : CongruenceSubgroup.IsCongruenceSubgroup H) : CongruenceSubgroup.IsCongruenceSubgroup K

theorem CongruenceSubgroup.Gamma_is_cong_sub (N : ℕ+) : CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma ↑N)

theorem CongruenceSubgroup.Gamma1_is_congruence (N : ℕ+) : CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma1 ↑N)

theorem CongruenceSubgroup.Gamma0_is_congruence (N : ℕ+) : CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma0 ↑N)

theorem CongruenceSubgroup.Gamma_cong_eq_self (N : ℕ) (g : ConjAct (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : g • CongruenceSubgroup.Gamma N = CongruenceSubgroup.Gamma N

theorem CongruenceSubgroup.conj_cong_is_cong (g : ConjAct (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (h : CongruenceSubgroup.IsCongruenceSubgroup Γ) : CongruenceSubgroup.IsCongruenceSubgroup (g • Γ)