tendsto_lcRow0 — Mathlib

English

For any coprime bottom row cd, the map g ↦ lcRow0 cd applied to ↑g, as g runs over SL(2,ℤ) with that bottom row, tends to cocompact in ℝ.

Русский

Для любой пары c,d взаимно простых нижняя строка, отображение g ↦ lcRow0(c,d) g, где g пробегает через SL(2,ℤ) с данной нижней строкой, стремится к конпактности в ℝ (т. е. образ сходится к бесконечности).

LaTeX

$$$\\forall \\text{cd with } \\gcd(cd_0,cd_1)=1,\\; Tendsto( g\\mapsto lcRow0(cd) \\; g) \\text{ к } \\text{cocompact}(\\mathbb{R}).$$$

Lean4

/-- The map `lcRow0` is proper, that is, preimages of cocompact sets are finite in
`[[* , *], [c, d]]`. -/
theorem tendsto_lcRow0 {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) :
    Tendsto (fun g : { g : SL(2, ℤ) // g 1 = cd } => lcRow0 cd ↑(↑g : SL(2, ℝ))) cofinite (cocompact ℝ) :=
  by
  let mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, (-(1 : ℤ) : ℝ)], (↑) ∘ cd]
  have hmB : Continuous mB := by
    refine continuous_matrix ?_
    simp only [mB, Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero, cons_val_one,
      and_self_iff]
  refine Filter.Tendsto.of_tendsto_comp ?_ (comap_cocompact_le hmB)
  let f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g => Matrix.map (↑g : Matrix _ _ ℤ) ((↑) : ℤ → ℝ)
  have cocompact_ℝ_to_cofinite_ℤ_matrix :
    Tendsto (fun m : Matrix (Fin 2) (Fin 2) ℤ => Matrix.map m ((↑) : ℤ → ℝ)) cofinite (cocompact _) := by
    simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using
      Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite
  have hf₁ : Tendsto f₁ cofinite (cocompact _) :=
    cocompact_ℝ_to_cofinite_ℤ_matrix.comp Subtype.coe_injective.tendsto_cofinite
  have hf₂ : IsClosedEmbedding (lcRow0Extend hcd) :=
    (lcRow0Extend hcd).toContinuousLinearEquiv.toHomeomorph.isClosedEmbedding
  convert hf₂.tendsto_cocompact.comp (hf₁.comp Subtype.coe_injective.tendsto_cofinite) using 1
  ext ⟨g, rfl⟩ i j : 3
  fin_cases i <;> [fin_cases j; skip]
    -- the following are proved by `simp`, but it is replaced by `simp only` to avoid timeouts.

  ·
    simp only [Fin.isValue, Int.cast_one, map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom, lcRow0_apply,
      map_apply, Fin.zero_eta, Function.comp_apply, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
      lcRow0Extend_apply, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
      val_planeConformalMatrix, neg_neg, mulVecLin_apply, mulVec, dotProduct, Fin.sum_univ_two, cons_val_one, mB, f₁]
  · convert congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
    simp only [Fin.zero_eta, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
      LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin, mulVecLin_apply, mulVec,
      dotProduct, det_fin_two, f₁]
    simp only [Fin.isValue, Fin.mk_one, val_planeConformalMatrix, neg_neg, of_apply, cons_val', empty_val',
      cons_val_fin_one, cons_val_one, map_apply, Fin.sum_univ_two, cons_val_zero, neg_mul, Int.cast_sub, Int.cast_mul,
      neg_sub]
    ring
  · rfl

Похожие утверждения