English
If hz : z ∈ 𝒟ᵒ and hg : g•z ∈ 𝒟ᵒ, then g_{1,0} = 0.
Русский
Если z ∈ 𝒟ᵒ и g•z ∈ 𝒟ᵒ, то g_{1,0} = 0.
LaTeX
$$$ z\in 𝒟^{\circ} \land (g\cdot z)\in 𝒟^{\circ} \Rightarrow g_{1,0} = 0$$$
Lean4
/-- An auxiliary result en route to `ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo`. -/
theorem c_eq_zero (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : g 1 0 = 0 :=
by
have hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → g' 1 0 ≠ 1 :=
by
intro g' hg'
by_contra hc
let a := g' 0 0
let d := g' 1 1
have had : T ^ (-a) * g' = S * T ^ d := by
rw [g_eq_of_c_eq_one hc]
dsimp [a, d]
group
let w := T ^ (-a) • g' • z
have h₁ : w = S • T ^ d • z := by simp only [w, ← mul_smul, had]
replace h₁ : normSq w < 1 := h₁.symm ▸ normSq_S_smul_lt_one (one_lt_normSq_T_zpow_smul hz d)
have h₂ : 1 < normSq w := one_lt_normSq_T_zpow_smul hg' (-a)
linarith
have hn : g 1 0 ≠ -1 := by
intro hc
replace hc : (-g) 1 0 = 1 := by simp [← neg_eq_iff_eq_neg.mpr hc]
replace hg : -g • z ∈ 𝒟ᵒ := (SL_neg_smul g z).symm ▸ hg
exact hp hg hc
specialize hp hg
rcases Int.abs_le_one_iff.mp <| abs_c_le_one hz hg with ⟨⟩ <;> tauto
