English
A cusp is precisely an SL(2, ℤ)-orbit of ∞.
Русский
К cusp является орбитой ∞ под действием SL(2, ℤ).
LaTeX
$$$IsCusp(c, \\mathcal{S L}) \\iff \\exists g \\in SL(2, \\mathbb{Z}), c = mapGL^\\mathbb{R}(g) \\cdot \\infty$$$
Lean4
/-- The cusps of `SL(2, ℤ)` are precisely the `SL(2, ℤ)` orbit of `∞`. -/
theorem isCusp_SL2Z_iff' {c : OnePoint ℝ} : IsCusp c 𝒮ℒ ↔ ∃ g : SL(2, ℤ), c = mapGL ℝ g • ∞ :=
by
rw [isCusp_SL2Z_iff]
constructor
· rintro ⟨c, rfl⟩
obtain ⟨g, rfl⟩ := c.exists_mem_SL2 ℤ
refine ⟨g, ?_⟩
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]
· rintro ⟨g, rfl⟩
refine ⟨mapGL ℚ g • ∞, ?_⟩
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty, ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]
