refactor(topology/instances): put ℕ, ℤ, and ℚ in separate files (…

…#12207)

The goal here is to make `metric_space ℕ` and `metric_space ℤ` available earlier, so that I can state `has_bounded_smul ℕ A` somewhere reasonable.

No lemmas have been added, deleted, or changed here - they've just been moved out of `topology/instances/real` and into 
`topology/instances/{nat,int,rat,real}`.

The resulting import structure is:
* `rat_lemmas` → `rat`
* `rat` → {`real`, `int`, `nat`}
* `real` → {`int`}
* `nat` → {`int`}

src/analysis/normed_space/basic.lean

@@ -9,6 +9,7 @@ import analysis.normed.group.infinite_sum
 import data.matrix.basic
 import topology.algebra.module.basic
 import topology.instances.ennreal
+import topology.instances.rat
 import topology.sequences
 
 /-!

src/topology/instances/int.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import topology.metric_space.basic
+import order.filter.archimedean
+/-!
+# Topology on the integers
+
+The structure of a metric space on `ℤ` is introduced in this file, induced from `ℝ`.
+-/
+noncomputable theory
+open metric set filter
+
+namespace int
+
+instance : has_dist ℤ := ⟨λ x y, dist (x : ℝ) y⟩
+
+theorem dist_eq (x y : ℤ) : dist x y = |x - y| := rfl
+
+@[norm_cast, simp] theorem dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y := rfl
+
+lemma pairwise_one_le_dist : pairwise (λ m n : ℤ, 1 ≤ dist m n) :=
+begin
+  intros m n hne,
+  rw dist_eq, norm_cast, rwa [← zero_add (1 : ℤ), int.add_one_le_iff, abs_pos, sub_ne_zero]
+end
+
+lemma uniform_embedding_coe_real : uniform_embedding (coe : ℤ → ℝ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+lemma closed_embedding_coe_real : closed_embedding (coe : ℤ → ℝ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+instance : metric_space ℤ := int.uniform_embedding_coe_real.comap_metric_space _
+
+theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
+
+theorem preimage_closed_ball (x : ℤ) (r : ℝ) :
+  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
+
+theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ :=
+by rw [← preimage_ball, real.ball_eq_Ioo, preimage_Ioo]
+
+theorem closed_ball_eq_Icc (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ :=
+by rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc]
+
+instance : proper_space ℤ :=
+⟨ begin
+    intros x r,
+    rw closed_ball_eq_Icc,
+    exact (set.finite_Icc _ _).is_compact,
+  end ⟩
+
+@[simp] lemma cocompact_eq : cocompact ℤ = at_bot ⊔ at_top :=
+by simp only [← comap_dist_right_at_top_eq_cocompact (0 : ℤ), dist_eq, sub_zero, cast_zero,
+  ← cast_abs, ← @comap_comap _ _ _ _ abs, int.comap_coe_at_top, comap_abs_at_top]
+
+@[simp] lemma cofinite_eq : (cofinite : filter ℤ) = at_bot ⊔ at_top :=
+by rw [← cocompact_eq_cofinite, cocompact_eq]
+
+end int

src/topology/instances/nat.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import topology.instances.int
+/-!
+# Topology on the natural numbers
+
+The structure of a metric space on `ℕ` is introduced in this file, induced from `ℝ`.
+-/
+noncomputable theory
+open metric set filter
+
+namespace nat
+
+noncomputable instance : has_dist ℕ := ⟨λ x y, dist (x : ℝ) y⟩
+
+theorem dist_eq (x y : ℕ) : dist x y = |x - y| := rfl
+
+lemma dist_coe_int (x y : ℕ) : dist (x : ℤ) (y : ℤ) = dist x y := rfl
+
+@[norm_cast, simp] theorem dist_cast_real (x y : ℕ) : dist (x : ℝ) y = dist x y := rfl
+
+lemma pairwise_one_le_dist : pairwise (λ m n : ℕ, 1 ≤ dist m n) :=
+begin
+  intros m n hne,
+  rw ← dist_coe_int,
+  apply int.pairwise_one_le_dist,
+  exact_mod_cast hne
+end
+
+lemma uniform_embedding_coe_real : uniform_embedding (coe : ℕ → ℝ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+lemma closed_embedding_coe_real : closed_embedding (coe : ℕ → ℝ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+instance : metric_space ℕ := nat.uniform_embedding_coe_real.comap_metric_space _
+
+theorem preimage_ball (x : ℕ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
+
+theorem preimage_closed_ball (x : ℕ) (r : ℝ) :
+  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
+
+theorem closed_ball_eq_Icc (x : ℕ) (r : ℝ) :
+  closed_ball x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊ :=
+begin
+  rcases le_or_lt 0 r with hr|hr,
+  { rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc],
+    exact add_nonneg (cast_nonneg x) hr },
+  { rw closed_ball_eq_empty.2 hr,
+    apply (Icc_eq_empty _).symm,
+    rw not_le,
+    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ : by { apply floor_mono, linarith }
+    ... < ⌈↑x - r⌉₊ : by { rw [floor_coe, nat.lt_ceil], linarith } }
+end
+
+instance : proper_space ℕ :=
+⟨ begin
+    intros x r,
+    rw closed_ball_eq_Icc,
+    exact (set.finite_Icc _ _).is_compact,
+  end ⟩
+
+instance : noncompact_space ℕ :=
+noncompact_space_of_ne_bot $ by simp [filter.at_top_ne_bot]
+
+end nat

src/topology/instances/rat.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import topology.metric_space.basic
+import topology.instances.int
+import topology.instances.nat
+import topology.instances.real
+/-!
+# Topology on the ratonal numbers
+
+The structure of a metric space on `ℚ` is introduced in this file, induced from `ℝ`.
+-/
+noncomputable theory
+open metric set filter
+
+namespace rat
+
+instance : metric_space ℚ :=
+metric_space.induced coe rat.cast_injective real.metric_space
+
+theorem dist_eq (x y : ℚ) : dist x y = |x - y| := rfl
+
+@[norm_cast, simp] lemma dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y := rfl
+
+theorem uniform_continuous_coe_real : uniform_continuous (coe : ℚ → ℝ) :=
+uniform_continuous_comap
+
+theorem uniform_embedding_coe_real : uniform_embedding (coe : ℚ → ℝ) :=
+uniform_embedding_comap rat.cast_injective
+
+theorem dense_embedding_coe_real : dense_embedding (coe : ℚ → ℝ) :=
+uniform_embedding_coe_real.dense_embedding $
+λ x, mem_closure_iff_nhds.2 $ λ t ht,
+let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
+let ⟨q, h⟩ := exists_rat_near x ε0 in
+⟨_, hε (mem_ball'.2 h), q, rfl⟩
+
+theorem embedding_coe_real : embedding (coe : ℚ → ℝ) := dense_embedding_coe_real.to_embedding
+
+theorem continuous_coe_real : continuous (coe : ℚ → ℝ) := uniform_continuous_coe_real.continuous
+
+end rat
+
+@[norm_cast, simp] theorem nat.dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y :=
+by rw [← nat.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
+
+lemma nat.uniform_embedding_coe_rat : uniform_embedding (coe : ℕ → ℚ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using nat.pairwise_one_le_dist
+
+lemma nat.closed_embedding_coe_rat : closed_embedding (coe : ℕ → ℚ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using nat.pairwise_one_le_dist
+
+@[norm_cast, simp] theorem int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=
+by rw [← int.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
+
+lemma int.uniform_embedding_coe_rat : uniform_embedding (coe : ℤ → ℚ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using int.pairwise_one_le_dist
+
+lemma int.closed_embedding_coe_rat : closed_embedding (coe : ℤ → ℚ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using int.pairwise_one_le_dist
+
+instance : noncompact_space ℚ := int.closed_embedding_coe_rat.noncompact_space
+
+-- TODO(Mario): Find a way to use rat_add_continuous_lemma
+theorem rat.uniform_continuous_add : uniform_continuous (λp : ℚ × ℚ, p.1 + p.2) :=
+rat.uniform_embedding_coe_real.to_uniform_inducing.uniform_continuous_iff.2 $
+  by simp only [(∘), rat.cast_add]; exact real.uniform_continuous_add.comp
+    (rat.uniform_continuous_coe_real.prod_map rat.uniform_continuous_coe_real)
+
+theorem rat.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℚ _) :=
+metric.uniform_continuous_iff.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
+  by rw dist_comm at h; simpa [rat.dist_eq] using h⟩
+
+instance : uniform_add_group ℚ :=
+uniform_add_group.mk' rat.uniform_continuous_add rat.uniform_continuous_neg
+
+instance : topological_add_group ℚ := by apply_instance
+
+instance : order_topology ℚ :=
+induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)
+
+lemma rat.uniform_continuous_abs : uniform_continuous (abs : ℚ → ℚ) :=
+metric.uniform_continuous_iff.2 $ λ ε ε0,
+  ⟨ε, ε0, λ a b h, lt_of_le_of_lt
+    (by simpa [rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩
+
+lemma rat.continuous_mul : continuous (λp : ℚ × ℚ, p.1 * p.2) :=
+rat.embedding_coe_real.continuous_iff.2 $ by simp [(∘)]; exact
+real.continuous_mul.comp ((rat.continuous_coe_real.prod_map rat.continuous_coe_real))
+
+instance : topological_ring ℚ :=
+{ continuous_mul := rat.continuous_mul, ..rat.topological_add_group }
+
+lemma rat.totally_bounded_Icc (a b : ℚ) : totally_bounded (Icc a b) :=
+begin
+  have := totally_bounded_preimage rat.uniform_embedding_coe_real (totally_bounded_Icc a b),
+  rwa (set.ext (λ q, _) : Icc _ _ = _), simp
+end