Modular group and congruence subgroups

TheoremMembership in a subgroup joined with a central involution#✓fully proved

Membership in the join of a subgroup with the cyclic subgroup generated by a central involution.

This is the computation behind "up to sign" arguments: for a subgroup Γ of SL(2, ℤ), an element lies in Γ adjoined with -1 exactly when it or its negative lies in Γ. The same pattern recurs for any group with a central involution: spin groups, dihedral groups, and congruence subgroups.

theorem mem_sup_zpowers_iff_of_central_sq_eq_one {G : Type*} [Group G]
    (Γ : Subgroup G) {c : G} (hc : c ∈ Subgroup.center G) (hc2 : c ^ 2 = 1)
    (g : G) :
    g ∈ Γ ⊔ Subgroup.zpowers c ↔ g ∈ Γ ∨ c * g ∈ Γ

TheoremReduction mod p maps Γ(N) onto SL(2, ℤ/pℤ) when p does not divide N#✓fully proved

If p does not divide N, then reduction modulo p maps Γ(N) onto SL(2, ZMod p).

theorem exists_mem_Gamma_map_eq_of_not_dvd
    (N p : ℕ) [NeZero N] [Fact p.Prime] (hpN : ¬ p ∣ N) :
    ∀ g : SL(2, ZMod p), ∃ γ : SL(2, ℤ), γ ∈ CongruenceSubgroup.Gamma N ∧
        Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod p)) γ = g

Theorem−1 lies in Γ₁(N) exactly when N ≤ 2#✓fully proved

-1 lies in Γ₁(N) if and only if N ≤ 2.

theorem neg_one_mem_Gamma1_iff (N : ℕ) [NeZero N] :
    (-1 : SL(2, ℤ)) ∈ CongruenceSubgroup.Gamma1 N ↔ N ≤ 2

TheoremParabolic elements of SL(2, ℤ) are conjugate to ± powers of T#✓fully proved

Every element of SL(2, ℤ) whose trace squares to 4 is, up to a sign, conjugate to a power of the translation T.

theorem exists_eq_conj_T_zpow_of_trace_sq_eq_four (γ : SL(2, ℤ))
    (hγ : ((γ : Matrix (Fin 2) (Fin 2) ℤ).trace) ^ 2 = 4) :
    ∃ (ε δ : SL(2, ℤ)) (h : ℤ), (ε = 1 ∨ ε = -1) ∧
      γ = ε * (δ * ModularGroup.T ^ h * δ⁻¹)

Theorem1 is a strict period of Γ₀(N)#✓fully proved

1 is a strict period of Γ₀(N): the translation matrix T lies in Γ₀(N), and the strict periods then contain the integer multiples of 1.

theorem CongruenceSubgroup.one_mem_strictPeriods_Gamma0 (N : ℕ) :
    (1 : ℝ) ∈ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma0 N)).strictPeriods

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.