feat(topology/instances/real): classify discrete subgroups (#16592)

The subgroups aℤ (i.e. `zmultiples a`) of ℝ are discrete, in the sense of having finite intersection with any compact subset.

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>

src/group_theory/subgroup/basic.lean

@@ -2035,6 +2035,15 @@ cod_restrict f _ $ λ x, ⟨x, rfl⟩
 @[simp, to_additive]
 lemma coe_range_restrict (f : G →* N) (g : G) : (f.range_restrict g : N) = f g := rfl
 
+@[to_additive]
+lemma coe_comp_range_restrict (f : G →* N) :
+  (coe : f.range → N) ∘ (⇑(f.range_restrict) : G → f.range) = f :=
+rfl
+
+@[to_additive]
+lemma subtype_comp_range_restrict (f : G →* N) : f.range.subtype.comp (f.range_restrict) = f :=
+ext $ f.coe_range_restrict
+
 @[to_additive]
 lemma range_restrict_surjective (f : G →* N) : function.surjective f.range_restrict :=
 λ ⟨_, g, rfl⟩, ⟨g, rfl⟩

src/topology/algebra/field.lean

@@ -63,7 +63,21 @@ instance top_monoid_units [topological_semiring R] [induced_units R] :
 end⟩
 end topological_ring
 
-variables (K : Type*) [division_ring K] [topological_space K]
+variables {K : Type*} [division_ring K] [topological_space K]
+
+/-- Left-multiplication by a nonzero element of a topological division ring is proper, i.e.,
+inverse images of compact sets are compact. -/
+lemma filter.tendsto_cocompact_mul_left₀ [has_continuous_mul K] {a : K} (ha : a ≠ 0) :
+  filter.tendsto (λ x : K, a * x) (filter.cocompact K) (filter.cocompact K) :=
+filter.tendsto_cocompact_mul_left (inv_mul_cancel ha)
+
+/-- Right-multiplication by a nonzero element of a topological division ring is proper, i.e.,
+inverse images of compact sets are compact. -/
+lemma filter.tendsto_cocompact_mul_right₀ [has_continuous_mul K] {a : K} (ha : a ≠ 0) :
+  filter.tendsto (λ x : K, x * a) (filter.cocompact K) (filter.cocompact K) :=
+filter.tendsto_cocompact_mul_right (mul_inv_cancel ha)
+
+variables (K)
 
 /-- A topological division ring is a division ring with a topology where all operations are
     continuous, including inversion. -/

src/topology/algebra/monoid.lean

@@ -417,6 +417,28 @@ lemma continuous_on.pow {f : X → M} {s : set X} (hf : continuous_on f s) (n :
   continuous_on (λ x, f x ^ n) s :=
 λ x hx, (hf x hx).pow n
 
+/-- Left-multiplication by a left-invertible element of a topological monoid is proper, i.e.,
+inverse images of compact sets are compact. -/
+lemma filter.tendsto_cocompact_mul_left {a b : M} (ha : b * a = 1) :
+  filter.tendsto (λ x : M, a * x) (filter.cocompact M) (filter.cocompact M) :=
+begin
+  refine filter.tendsto.of_tendsto_comp _ (filter.comap_cocompact_le (continuous_mul_left b)),
+  convert filter.tendsto_id,
+  ext x,
+  simp [ha],
+end
+
+/-- Right-multiplication by a right-invertible element of a topological monoid is proper, i.e.,
+inverse images of compact sets are compact. -/
+lemma filter.tendsto_cocompact_mul_right {a b : M} (ha : a * b = 1) :
+  filter.tendsto (λ x : M, x * a) (filter.cocompact M) (filter.cocompact M) :=
+begin
+  refine filter.tendsto.of_tendsto_comp _ (filter.comap_cocompact_le (continuous_mul_right b)),
+  convert filter.tendsto_id,
+  ext x,
+  simp [ha],
+end
+
 /-- If `R` acts on `A` via `A`, then continuous multiplication implies continuous scalar
 multiplication by constants.
 

src/topology/instances/real.lean

@@ -216,6 +216,52 @@ end periodic
 
 section subgroups
 
+namespace int
+open metric
+
+/-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
+lemma tendsto_coe_cofinite : tendsto (coe : ℤ → ℝ) cofinite (cocompact ℝ) :=
+begin
+  refine tendsto_cocompact_of_tendsto_dist_comp_at_top (0 : ℝ) _,
+  simp only [filter.tendsto_at_top, eventually_cofinite, not_le, ← mem_ball],
+  change ∀ r : ℝ, (coe ⁻¹' (ball (0 : ℝ) r)).finite,
+  simp [real.ball_eq_Ioo, set.finite_Ioo],
+end
+
+/-- For nonzero `a`, the "multiples of `a`" map `zmultiples_hom` from `ℤ` to `ℝ` is discrete, i.e.
+inverse images of compact sets are finite. -/
+lemma tendsto_zmultiples_hom_cofinite {a : ℝ} (ha : a ≠ 0) :
+  tendsto (zmultiples_hom ℝ a) cofinite (cocompact ℝ) :=
+begin
+  convert (tendsto_cocompact_mul_right₀ ha).comp int.tendsto_coe_cofinite,
+  ext n,
+  simp,
+end
+
+end int
+
+namespace add_subgroup
+
+/-- The subgroup "multiples of `a`" (`zmultiples a`) is a discrete subgroup of `ℝ`, i.e. its
+intersection with compact sets is finite. -/
+lemma tendsto_zmultiples_subtype_cofinite (a : ℝ) :
+  tendsto (zmultiples a).subtype cofinite (cocompact ℝ) :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha,
+  { rw add_subgroup.zmultiples_zero_eq_bot,
+    intros K hK,
+    rw [filter.mem_map, mem_cofinite],
+    apply set.to_finite },
+  intros K hK,
+  have H := int.tendsto_zmultiples_hom_cofinite ha hK,
+  simp only [filter.mem_map, mem_cofinite, ← preimage_compl] at ⊢ H,
+  rw [← (zmultiples_hom ℝ a).range_restrict_surjective.image_preimage
+    ((zmultiples a).subtype ⁻¹' Kᶜ), ← preimage_comp, ← add_monoid_hom.coe_comp_range_restrict],
+  exact finite.image _ H,
+end
+
+end add_subgroup
+
 /-- Given a nontrivial subgroup `G ⊆ ℝ`, if `G ∩ ℝ_{>0}` has no minimum then `G` is dense. -/
 lemma real.subgroup_dense_of_no_min {G : add_subgroup ℝ} {g₀ : ℝ} (g₀_in : g₀ ∈ G) (g₀_ne : g₀ ≠ 0)
   (H' : ¬ ∃ a : ℝ, is_least {g : ℝ | g ∈ G ∧ 0 < g} a) :

src/topology/metric_space/basic.lean

@@ -2489,20 +2489,6 @@ lemma tendsto_cocompact_of_tendsto_dist_comp_at_top {f : β → α} {l : filter
   (h : tendsto (λ y, dist (f y) x) l at_top) : tendsto f l (cocompact α) :=
 by { refine tendsto.mono_right _ (comap_dist_right_at_top_le_cocompact x), rwa tendsto_comap_iff }
 
-namespace int
-open metric
-
-/-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
-lemma tendsto_coe_cofinite : tendsto (coe : ℤ → ℝ) cofinite (cocompact ℝ) :=
-begin
-  refine tendsto_cocompact_of_tendsto_dist_comp_at_top (0 : ℝ) _,
-  simp only [filter.tendsto_at_top, eventually_cofinite, not_le, ← mem_ball],
-  change ∀ r : ℝ, (coe ⁻¹' (ball (0 : ℝ) r)).finite,
-  simp [real.ball_eq_Ioo, set.finite_Ioo],
-end
-
-end int
-
 /-- We now define `metric_space`, extending `pseudo_metric_space`. -/
 class metric_space (α : Type u) extends pseudo_metric_space α : Type u :=
 (eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)