English
There is a canonical map cosetToCuspOrbit from SL(2, ℤ) cosets to cusp orbits of 𝒢 (assuming arithmetic).
Русский
Существует каноническое отображение cosetToCuspOrbit от косет SL(2, ℤ) к cusp-орбитам 𝒢 (при условии арифметичности).
LaTeX
$$$\\cosetToCuspOrbit(\\mathcal{G}) : SL(2, \\mathbb{Z}) / (\\mathcal{G}.comap(\\mathrm{mapGL} \\mathbb{R})) \\to \\mathrm{CuspOrbits}(\\mathcal{G})$$$
Lean4
/-- Surjection from `SL(2, ℤ) / (𝒢 ⊓ SL(2, ℤ))` to cusp orbits of `𝒢`. Mostly useful for showing
that `CuspOrbits 𝒢` is finite for arithmetic subgroups. -/
noncomputable def cosetToCuspOrbit (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] :
SL(2, ℤ) ⧸ (𝒢.comap <| mapGL ℝ) → CuspOrbits 𝒢 :=
Quotient.lift
(fun g ↦
⟦⟨mapGL ℝ g⁻¹ • ∞,
(Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z 𝒢).mpr <|
isCusp_SL2Z_iff.mpr
⟨mapGL ℚ g⁻¹ • ∞, by
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, ← (Rat.castHom ℝ).algebraMap_toAlgebra,
map_mapGL]⟩⟩⟧)
(fun a b hab ↦ by
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hab
refine Quotient.eq.mpr ⟨⟨_, hab⟩, ?_⟩
simp [MulAction.mul_smul])
