Γ_Δ(N), ε_Δ, h_Δ: basic facts

• membership in Γ_Δ(N) and its image in SL₂(ℝ); T, U ∈ Γ_Δ(N);
• ε_Δ ∣ N and ε_Δ ∣ d² − 1 for d ∈ Δ (dvd_epsDelta_iff), hence every element of Γ_Δ(N) lies in the lattice L_{ε_Δ} (inLe_of_mem_GammaDeltaR);
• v_p(h_Δ) = min(v_p(ε_Δ), ⌊v_p(N)/2⌋) (factorization_hDelta);
• the element γ_p ∈ Γ_Δ(N) (exists_gamma_delta): if v_p(ε_Δ) < v_p(N), some d ∈ Δ has v_p(d² − 1) = v_p(ε_Δ), and [[x, y], [N, d]] has v_p(d − x) = v_p(ε_Δ).

theorem CongruenceNormalizers.mem_toR {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} : g ∈ toR Γ ↔ ∃ γ ∈ Γ, ofZ γ = g

theorem CongruenceNormalizers.ofZ_mem_toR {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (h : γ ∈ Γ) : ofZ γ ∈ toR Γ

theorem CongruenceNormalizers.coe_ofZ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(ofZ γ) = !![↑(↑γ 0 0), ↑(↑γ 0 1); ↑(↑γ 1 0), ↑(↑γ 1 1)]

theorem CongruenceNormalizers.GammaDelta_le_Gamma0 {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} : GammaDelta N Δ ≤ CongruenceSubgroup.Gamma0 N

theorem CongruenceNormalizers.GammaDeltaR_le_Gamma0R {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} : GammaDeltaR N Δ ≤ Gamma0R N

def CongruenceNormalizers.mkSL (a b c d : ℤ) (h : a * d - b * c = 1) : Matrix.SpecialLinearGroup (Fin 2) ℤ

An integer matrix of determinant 1.

Equations

• CongruenceNormalizers.mkSL a b c d h = ⟨!![a, b; c, d], ⋯⟩

theorem CongruenceNormalizers.mkSL_mem_GammaDelta {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} {a b c d : ℤ} (h : a * d - b * c = 1) (hc : ↑N ∣ c) {u : (ZMod N)ˣ} (hu : u ∈ Δ) (hud : ↑u = ↑d) : mkSL a b c d h ∈ GammaDelta N Δ

theorem CongruenceNormalizers.coe_ofZ_mkSL {a b c d : ℤ} (h : a * d - b * c = 1) : ↑(ofZ (mkSL a b c d h)) = !![↑a, ↑b; ↑c, ↑d]

theorem CongruenceNormalizers.matT_mem_GammaDeltaR {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} : matT ∈ GammaDeltaR N Δ

theorem CongruenceNormalizers.matU_mem_GammaDeltaR {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} : matU N ∈ GammaDeltaR N Δ

ε_Δ

theorem CongruenceNormalizers.dvd_epsDelta_iff {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] {m : ℕ} : m ∣ epsDelta N Δ ↔ m ∣ N ∧ ∀ u ∈ Δ, m ∣ (↑u).val ^ 2 - 1

theorem CongruenceNormalizers.epsDelta_dvd {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] : epsDelta N Δ ∣ N

theorem CongruenceNormalizers.epsDelta_dvd_val {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] {u : (ZMod N)ˣ} (hu : u ∈ Δ) : epsDelta N Δ ∣ (↑u).val ^ 2 - 1

theorem CongruenceNormalizers.epsDelta_pos {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] : 0 < epsDelta N Δ

theorem CongruenceNormalizers.one_le_val_unit {N : ℕ} (hN : 2 ≤ N) (u : (ZMod N)ˣ) : 1 ≤ (↑u).val

For N ≥ 2 a unit has a positive representative.

theorem CongruenceNormalizers.epsDelta_dvd_val_int {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] {u : (ZMod N)ˣ} (hu : u ∈ Δ) : ↑(epsDelta N Δ) ∣ ↑(↑u).val ^ 2 - 1

The integer form of ε_Δ ∣ val(u)² − 1.

theorem CongruenceNormalizers.inLe_of_mem_GammaDeltaR {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] {Y : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hY : Y ∈ GammaDeltaR N Δ) : InLe N (epsDelta N Δ) ↑Y

Every element of Γ_Δ(N) lies in the lattice L_{ε_Δ}.

h_Δ

theorem CongruenceNormalizers.factorization_hDelta {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} [NeZero N] (p : ℕ) : (hDelta N Δ).factorization p = min ((epsDelta N Δ).factorization p) (N.factorization p / 2)