English
Gamma0 is a finite-index subgroup for NeZero N.
Русский
Γ0 является подгруппой с конечным индексом при N ≠ 0.
LaTeX
$$$$ [NeZero\ N] \Rightarrow (\Gamma_0(N)).FiniteIndex. $$$$
Lean4
/-- If `Γ` has finite index in `SL(2, ℤ)`, then so does `g⁻¹ Γ g ∩ SL(2, ℤ)` for any
`g ∈ GL(2, ℚ)`. -/
theorem finiteIndex_conjGL (g : GL (Fin 2) ℚ) : (conjGL ⊤ (g.map <| Rat.castHom ℝ)).FiniteIndex :=
by
constructor
let t := (toConjAct <| g.map <| Rat.castHom ℝ)⁻¹
suffices (t • 𝒮ℒ ⊓ 𝒮ℒ).relIndex 𝒮ℒ ≠ 0 by rwa [conjGL, index_comap, ← inf_relIndex_right, ← MonoidHom.range_eq_map]
obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g 1
rw [Gamma_one_top, ← MonoidHom.range_eq_map] at hN'
suffices Γ(N) ≤ (t • 𝒮ℒ ⊓ 𝒮ℒ).comap (mapGL ℝ)
by
haveI _ : NeZero N := ⟨hN⟩
simpa only [index_comap] using (finiteIndex_of_le this).index_ne_zero
intro k hk
simpa [mem_pointwise_smul_iff_inv_smul_mem] using hN' <| smul_mem_pointwise_smul _ _ _ ⟨k, hk, rfl⟩
