English
The cusps of SL(2, ℤ) are precisely the points c of ℙ¹(ℚ).
Русский
Уступы SL(2, ℤ) совпадают с точками ℙ¹(ℚ).
LaTeX
$$$IsCusp(c, \\mathcal{S L}) \\iff c \\in \\operatorname{range}(\\mathrm{OnePoint.map}(\\mathrm{Rat.cast}))$$$
Lean4
/-- The cusps of `SL(2, ℤ)` are precisely the elements of `ℙ¹(ℚ)`. -/
theorem isCusp_SL2Z_iff {c : OnePoint ℝ} : IsCusp c 𝒮ℒ ↔ c ∈ Set.range (OnePoint.map Rat.cast) :=
by
constructor
· rintro ⟨-, ⟨g, rfl⟩, hgp, hgc⟩
simpa only [hgp.smul_eq_self_iff.mp hgc] using
⟨(mapGL ℚ g).parabolicFixedPoint, by simp [GeneralLinearGroup.parabolicFixedPoint, apply_ite]⟩
· rintro ⟨c, rfl⟩
obtain ⟨a, rfl⟩ := c.exists_mem_SL2 ℤ
refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩
· suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa
refine ⟨fun ⟨a, ha⟩ ↦ zero_ne_one' ℝ (by simpa [ModularGroup.T] using congr_fun₂ ha 0 1), ?_⟩
simp [disc_fin_two, trace_fin_two, det_fin_two, ModularGroup.T]
norm_num
· rw [← Rat.coe_castHom, ← (Rat.castHom ℝ).algebraMap_toAlgebra]
simp [OnePoint.map_smul, MulAction.mul_smul, smul_infty_eq_self_iff, ModularGroup.T]
