English
The application of cosetToCuspOrbit to a representative g ∈ SL(2, ℤ) matches the explicit cusp described by g⁻¹ acting on ∞.
Русский
Применение cosetToCuspOrbit к представителю g ∈ SL(2, ℤ) совпадает с явным cusp, задаваемым g⁻¹, действующим на ∞.
LaTeX
$$$\\cosetToCuspOrbit(\\mathcal{G}) \\; \\langle g \\rangle = \\; \\langle mapGL(\\mathbb{R}) \\; g^{-1} \\cdot \\infty, \\; \\dots \\rangle$$$
Lean4
@[simp]
theorem cosetToCuspOrbit_apply_mk {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] (g : SL(2, ℤ)) :
cosetToCuspOrbit 𝒢 ⟦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]⟩⟩⟧ :=
rfl
