feat: basic facts about discrete subsets and subgroups (#5969)

Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>

Mathlib.lean

@@ -3225,6 +3225,7 @@ import Mathlib.Topology.CountableSeparatingOn
 import Mathlib.Topology.Covering
 import Mathlib.Topology.DenseEmbedding
 import Mathlib.Topology.DiscreteQuotient
+import Mathlib.Topology.DiscreteSubset
 import Mathlib.Topology.ExtendFrom
 import Mathlib.Topology.ExtremallyDisconnected
 import Mathlib.Topology.FiberBundle.Basic

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -163,7 +163,8 @@ theorem frontier_sphere [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : r ≠ 0) :
   rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]
 #align frontier_sphere frontier_sphere
 
-instance {E : Type _} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :
+instance NormedSpace.discreteTopology_zmultiples
+    {E : Type _} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :
     DiscreteTopology <| AddSubgroup.zmultiples e := by
   rcases eq_or_ne e 0 with (rfl | he)
   · rw [AddSubgroup.zmultiples_zero_eq_bot]

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -2642,6 +2642,10 @@ theorem rangeRestrict_surjective (f : G →* N) : Function.Surjective f.rangeRes
 #align monoid_hom.range_restrict_surjective MonoidHom.rangeRestrict_surjective
 #align add_monoid_hom.range_restrict_surjective AddMonoidHom.rangeRestrict_surjective
 
+@[to_additive (attr := simp)]
+lemma rangeRestrict_injective_iff {f : G →* N} : Injective f.rangeRestrict ↔ Injective f := by
+  convert Set.injective_codRestrict _
+
 @[to_additive]
 theorem map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range := by
   rw [range_eq_map, range_eq_map]; exact (⊤ : Subgroup G).map_map g f

Mathlib/GroupTheory/Subgroup/ZPowers.lean

@@ -148,6 +148,11 @@ end Ring
 
 end AddSubgroup
 
+@[simp] lemma Int.range_castAddHom {A : Type _} [AddGroupWithOne A] :
+    (Int.castAddHom A).range = AddSubgroup.zmultiples 1 := by
+  ext a
+  simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]
+
 @[to_additive (attr := simp) map_zmultiples]
 theorem MonoidHom.map_zpowers (f : G →* N) (x : G) :
     (Subgroup.zpowers x).map f = Subgroup.zpowers (f x) := by

Mathlib/Topology/Algebra/UniformGroup.lean

@@ -8,6 +8,7 @@ import Mathlib.Topology.UniformSpace.UniformEmbedding
 import Mathlib.Topology.UniformSpace.CompleteSeparated
 import Mathlib.Topology.UniformSpace.Compact
 import Mathlib.Topology.Algebra.Group.Basic
+import Mathlib.Topology.DiscreteSubset
 import Mathlib.Tactic.Abel
 
 #align_import topology.algebra.uniform_group from "leanprover-community/mathlib"@"bcfa726826abd57587355b4b5b7e78ad6527b7e4"
@@ -606,6 +607,18 @@ instance Subgroup.isClosed_of_discrete [T2Space G] {H : Subgroup G} [DiscreteTop
 #align subgroup.is_closed_of_discrete Subgroup.isClosed_of_discrete
 #align add_subgroup.is_closed_of_discrete AddSubgroup.isClosed_of_discrete
 
+@[to_additive]
+lemma Subgroup.tendsto_coe_cofinite_of_discrete [T2Space G] (H : Subgroup G) [DiscreteTopology H] :
+    Tendsto ((↑) : H → G) cofinite (cocompact _) :=
+  IsClosed.tendsto_coe_cofinite_of_discreteTopology inferInstance inferInstance
+
+@[to_additive]
+lemma MonoidHom.tendsto_coe_cofinite_of_discrete [T2Space G] {H : Type _} [Group H] {f : H →* G}
+    (hf : Function.Injective f) (hf' : DiscreteTopology f.range) :
+    Tendsto f cofinite (cocompact _) := by
+  replace hf : Function.Injective f.rangeRestrict := by simpa
+  exact f.range.tendsto_coe_cofinite_of_discrete.comp hf.tendsto_cofinite
+
 @[to_additive]
 theorem TopologicalGroup.tendstoUniformly_iff {ι α : Type _} (F : ι → α → G) (f : α → G)
     (p : Filter ι) :

Mathlib/Topology/DiscreteSubset.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2023 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash, Bhavik Mehta
+-/
+import Mathlib.Topology.SubsetProperties
+import Mathlib.Topology.Separation
+
+/-!
+# Discrete subsets of topological spaces
+
+Given a topological space `X` together with a subset `s ⊆ X`, there are two distinct concepts of
+"discreteness" which may hold. These are:
+  (i) Every point of `s` is isolated (i.e., the subset topology induced on `s` is the discrete
+      topology).
+ (ii) Every compact subset of `X` meets `s` only finitely often (i.e., the inclusion map `s → X`
+      tends to the cocompact filter along the cofinite filter on `s`).
+
+When `s` is closed, the two conditions are equivalent provided `X` is locally compact and T1,
+see `IsClosed.tendsto_coe_cofinite_iff`.
+
+## Main statements
+
+ * `tendsto_cofinite_cocompact_iff`:
+ * `IsClosed.tendsto_coe_cofinite_iff`:
+
+-/
+
+open Set Filter Function Topology
+
+variable {X Y : Type _} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y}
+
+lemma tendsto_cofinite_cocompact_iff :
+    Tendsto f cofinite (cocompact _) ↔ ∀ K, IsCompact K → Set.Finite (f ⁻¹' K) := by
+  rw [hasBasis_cocompact.tendsto_right_iff]
+  refine' forall₂_congr (fun K _ ↦ _)
+  simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]
+
+lemma Continuous.discrete_of_tendsto_cofinite_cocompact [T1Space X] [LocallyCompactSpace Y]
+    (hf' : Continuous f) (hf : Tendsto f cofinite (cocompact _)) :
+    DiscreteTopology X := by
+  refine' singletons_open_iff_discrete.mp (fun x ↦ _)
+  obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)
+  obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'
+  have hU₄ : Set.Finite (f⁻¹' U) :=
+    Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
+  exact isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄
+
+lemma tendsto_cofinite_cocompact_of_discrete [DiscreteTopology X]
+    (hf : Tendsto f (cocompact _) (cocompact _)) :
+    Tendsto f cofinite (cocompact _) := by
+  convert hf
+  rw [cocompact_eq_cofinite X]
+
+lemma IsClosed.tendsto_coe_cofinite_of_discreteTopology
+    {s : Set X} (hs : IsClosed s) (_hs' : DiscreteTopology s) :
+    Tendsto ((↑) : s → X) cofinite (cocompact _) :=
+  tendsto_cofinite_cocompact_of_discrete hs.closedEmbedding_subtype_val.tendsto_cocompact
+
+lemma IsClosed.tendsto_coe_cofinite_iff [T1Space X] [LocallyCompactSpace X]
+    {s : Set X} (hs : IsClosed s) :
+    Tendsto ((↑) : s → X) cofinite (cocompact _) ↔ DiscreteTopology s :=
+  ⟨continuous_subtype_val.discrete_of_tendsto_cofinite_cocompact,
+   fun _ ↦ hs.tendsto_coe_cofinite_of_discreteTopology inferInstance⟩

Mathlib/Topology/Instances/Real.lean

@@ -227,21 +227,32 @@ namespace Int
 
 open Metric
 
+/-- This is a special case of `NormedSpace.discreteTopology_zmultiples`. It exists only to simplify
+dependencies. -/
+instance {a : ℝ} : DiscreteTopology (AddSubgroup.zmultiples a) := by
+  rcases eq_or_ne a 0 with (rfl | ha)
+  · rw [AddSubgroup.zmultiples_zero_eq_bot]
+    exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))
+  rw [discreteTopology_iff_open_singleton_zero, isOpen_induced_iff]
+  refine' ⟨ball 0 |a|, isOpen_ball, _⟩
+  ext ⟨x, hx⟩
+  obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
+  simp [ha, Real.dist_eq, abs_mul, (by norm_cast : |(k : ℝ)| < 1 ↔ |k| < 1)]
+
 /-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
 theorem tendsto_coe_cofinite : Tendsto ((↑) : ℤ → ℝ) cofinite (cocompact ℝ) := by
-  refine' tendsto_cocompact_of_tendsto_dist_comp_atTop (0 : ℝ) _
-  simp only [Filter.tendsto_atTop, eventually_cofinite, not_le, ← mem_ball]
-  change ∀ r : ℝ, (Int.cast ⁻¹' ball (0 : ℝ) r).Finite
-  simp [Real.ball_eq_Ioo, Set.finite_Ioo]
+  apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
+  rw [range_castAddHom]
+  infer_instance
 #align int.tendsto_coe_cofinite Int.tendsto_coe_cofinite
 
 /-- For nonzero `a`, the "multiples of `a`" map `zmultiplesHom` from `ℤ` to `ℝ` is discrete, i.e.
 inverse images of compact sets are finite. -/
 theorem tendsto_zmultiplesHom_cofinite {a : ℝ} (ha : a ≠ 0) :
     Tendsto (zmultiplesHom ℝ a) cofinite (cocompact ℝ) := by
-  convert (tendsto_cocompact_mul_right₀ ha).comp Int.tendsto_coe_cofinite
-  ext n
-  simp
+  apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete $ smul_left_injective ℤ ha
+  rw [AddSubgroup.range_zmultiplesHom]
+  infer_instance
 #align int.tendsto_zmultiples_hom_cofinite Int.tendsto_zmultiplesHom_cofinite
 
 end Int
@@ -251,14 +262,8 @@ namespace AddSubgroup
 /-- The subgroup "multiples of `a`" (`zmultiples a`) is a discrete subgroup of `ℝ`, i.e. its
 intersection with compact sets is finite. -/
 theorem tendsto_zmultiples_subtype_cofinite (a : ℝ) :
-    Tendsto (zmultiples a).subtype cofinite (cocompact ℝ) := by
-  rcases eq_or_ne a 0 with rfl | ha
-  · rw [zmultiples_zero_eq_bot, cofinite_eq_bot]; exact tendsto_bot
-  · calc cofinite.map (zmultiples a).subtype
-      ≤ .map (zmultiples a).subtype (.map (rangeFactorization (· • a)) (@cofinite ℤ)) :=
-        Filter.map_mono surjective_onto_range.le_map_cofinite
-    _ = (@cofinite ℤ).map (zmultiplesHom ℝ a) := Filter.map_map
-    _ ≤ cocompact ℝ := Int.tendsto_zmultiplesHom_cofinite ha
+    Tendsto (zmultiples a).subtype cofinite (cocompact ℝ) :=
+  (zmultiples a).tendsto_coe_cofinite_of_discrete
 #align add_subgroup.tendsto_zmultiples_subtype_cofinite AddSubgroup.tendsto_zmultiples_subtype_cofinite
 
 end AddSubgroup