English
The action of SL(2, A) on OnePoint(K) is transitive when A is a PID with fraction field K (e.g., Z and Q).
Русский
Действие SL(2, A) на OnePoint(K) тождественно транзитивно, когда A — PID с полем дробей K (например Z и Q).
LaTeX
$$$$ \exists g: SL(2,A) \text{ with } (mapGL K\, g) \cdot \infty = c. $$$$
Lean4
/-- The modular group `SL(2, A)` acts transitively on `OnePoint K`, if `A` is a PID whose fraction
field is `K`. (This includes the case `A = ℤ`, `K = ℚ`.) -/
theorem exists_mem_SL2 (A : Type*) [CommRing A] [IsDomain A] [Algebra A K] [IsFractionRing A K] [IsPrincipalIdealRing A]
(c : OnePoint K) : ∃ g : SL(2, A), (mapGL K g) • ∞ = c := by
cases c with
| infty => exact ⟨1, by simp⟩
| coe q =>
obtain ⟨g, hg0, hg1⟩ := (IsFractionRing.num_den_reduced A q).isCoprime.exists_SL2_col 0
exact ⟨g, by simp [hg0, hg1, smul_infty_eq_ite]⟩
