English
For a fixed z ∈ ℍ, the map (c,d) ↦ |c z + d|^2 on coprime pairs is proper; equivalently, preimages of bounded sets are finite.
Русский
Для фиксированного z ∈ ℍ отображение (c,d) ↦ |c z + d|^2 на взаимно простых парах циллиндров обратно вдоль ℤ^2 является правильным; предобраз множества ограниченной величины конечен.
LaTeX
$$$\\text{For fixed } z \\in \\mathbb{H},\\; (c,d) \\mapsto |c z + d|^2 \\text{ with } \\gcd(c,d)=1 \\text{ is a proper map; i.e., the preimage of any bounded set is finite.}$$$
Lean4
/-- The function `(c,d) → |cz+d|^2` is proper, that is, preimages of bounded-above sets are finite.
-/
theorem tendsto_normSq_coprime_pair :
Filter.Tendsto (fun p : Fin 2 → ℤ => normSq ((p 0 : ℂ) * z + p 1)) cofinite atTop := by
-- using this instance rather than the automatic `Function.module` makes unification issues in
-- `LinearEquiv.isClosedEmbedding_of_injective` less bad later in the proof.
letI : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
let π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
let π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
let f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight (z : ℂ) + π₁.smulRight 1
have f_def : ⇑f = fun p : Fin 2 → ℝ => (p 0 : ℂ) * ↑z + p 1 :=
by
ext1
dsimp only [π₀, π₁, f, LinearMap.coe_proj, real_smul, LinearMap.coe_smulRight, LinearMap.add_apply]
rw [mul_one]
have :
(fun p : Fin 2 → ℤ => normSq ((p 0 : ℂ) * ↑z + ↑(p 1))) = normSq ∘ f ∘ fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p :=
by
ext1
rw [f_def]
dsimp only [Function.comp_def]
rw [ofReal_intCast, ofReal_intCast]
rw [this]
have hf : LinearMap.ker f = ⊥ :=
by
let g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm.comp ((z : ℂ) • ((conjAe : ℂ →ₐ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ))]
suffices ((z : ℂ).im⁻¹ • g).comp f = LinearMap.id by exact LinearMap.ker_eq_bot_of_inverse this
apply LinearMap.ext
intro c
have hz : (z : ℂ).im ≠ 0 := z.2.ne'
rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]
ext i
dsimp only [Pi.smul_apply, LinearMap.pi_apply, smul_eq_mul]
fin_cases i
· change (z : ℂ).im⁻¹ * (f c).im = c 0
rw [f_def, add_im, im_ofReal_mul, ofReal_im, add_zero, mul_left_comm, inv_mul_cancel₀ hz, mul_one]
· change (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1
rw [f_def, RingHom.map_add, RingHom.map_mul, mul_add, mul_left_comm, mul_conj, conj_ofReal, conj_ofReal, ←
ofReal_mul, add_im, ofReal_im, zero_add, inv_mul_eq_iff_eq_mul₀ hz]
simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]
have hf' : IsClosedEmbedding f := f.isClosedEmbedding_of_injective hf
have h₂ : Tendsto (fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p) cofinite (cocompact _) :=
by
convert Tendsto.pi_map_coprodᵢ fun _ => Int.tendsto_coe_cofinite
· rw [coprodᵢ_cofinite]
· rw [coprodᵢ_cocompact]
exact tendsto_normSq_cocompact_atTop.comp (hf'.tendsto_cocompact.comp h₂)
