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.
The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity
modulo N.
Equations
Instances For
The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity
modulo N.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The congruence subgroup of SL(2, ℤ) of matrices whose lower left-hand entry reduces to zero
modulo N.
Equations
Instances For
The group homomorphism from CongruenceSubgroup.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' := ⋯ }
Instances For
The congruence subgroup Gamma1 of SL(2, ℤ) consisting of matrices
whose bottom row is congruent to (0,1) modulo N.
Equations
Instances For
A congruence subgroup is a subgroup of SL(2, ℤ) which contains some Gamma N for some
N ≠ 0.
Equations
- CongruenceSubgroup.IsCongruenceSubgroup Γ = ∃ (N : ℕ), N ≠ 0 ∧ CongruenceSubgroup.Gamma N ≤ Γ
Instances For
The subgroup SL(2, ℤ) ∩ g⁻¹ Γ g, for Γ a subgroup of SL(2, ℤ) and g ∈ GL(2, ℝ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of CongruenceSubgroup.conjGL.
The subgroup SL(2, ℤ) ∩ g⁻¹ Γ g, for Γ a subgroup of SL(2, ℤ) and g ∈ GL(2, ℝ).
Instances For
Alias of CongruenceSubgroup.conjGL_coe.
Alias of CongruenceSubgroup.mem_conjGL.
Alias of CongruenceSubgroup.mem_conjGL'.
For any g ∈ GL(2, ℚ) and M ≠ 0, there exists N such that g x g⁻¹ ∈ Γ(M) for all
x ∈ Γ(N).
For any g ∈ GL(2, ℚ) and M ≠ 0, there exists N such that g Γ(N) g⁻¹ ≤ Γ(M).
If Γ has finite index in SL(2, ℤ), then so does g⁻¹ Γ g ∩ SL(2, ℤ) for any
g ∈ GL(2, ℚ).
If Γ is a congruence subgroup, then so is g⁻¹ Γ g ∩ SL(2, ℤ) for any g ∈ GL(2, ℚ).