feat(topology/uniform_space/completion): add uniform_completion.compl…

…ete_equiv_self (#16612)

- Change ```abstract_completion.compare_equiv``` to uniform bijection.
- Define the ```abstract_completion α``` given by ```α``` when it is complete. 
- Use it to prove that there is a uniform bijection between a complete space and its ```uniform_completion```.
- Upgrade the bijection between ```Bourbaki reals``` and ```Cauchy reals``` to a uniform bijection. 
- Add a new function ```function.dense_range_id``` (needed in one of the proofs)

src/topology/basic.lean

@@ -1446,6 +1446,9 @@ variables {f}
 lemma function.surjective.dense_range (hf : function.surjective f) : dense_range f :=
 λ x, by simp [hf.range_eq]
 
+lemma dense_range_id : dense_range (id : α → α) :=
+function.surjective.dense_range function.surjective_id
+
 lemma dense_range_iff_closure_range : dense_range f ↔ closure (range f) = univ :=
 dense_iff_closure_eq
 

src/topology/uniform_space/abstract_completion.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import topology.uniform_space.uniform_embedding
+import topology.uniform_space.equiv
 
 /-!
 # Abstract theory of Hausdorff completions of uniform spaces
@@ -67,6 +68,10 @@ variables {α : Type*} [uniform_space α] (pkg : abstract_completion α)
 local notation `hatα` := pkg.space
 local notation `ι` := pkg.coe
 
+/-- If `α` is complete, then it is an abstract completion of itself. -/
+def of_complete [separated_space α] [complete_space α] : abstract_completion α :=
+mk α id infer_instance infer_instance infer_instance uniform_inducing_id dense_range_id
+
 lemma closure_range : closure (range ι) = univ :=
 pkg.dense.closure_range
 
@@ -222,12 +227,14 @@ begin
   refl
 end
 
-/-- The bijection between two completions of the same uniform space. -/
-def compare_equiv : pkg.space ≃ pkg'.space :=
+/-- The uniform bijection between two completions of the same uniform space. -/
+def compare_equiv : pkg.space ≃ᵤ pkg'.space :=
 { to_fun := pkg.compare pkg',
   inv_fun := pkg'.compare pkg,
   left_inv := congr_fun (pkg'.inverse_compare pkg),
-  right_inv := congr_fun (pkg.inverse_compare pkg') }
+  right_inv := congr_fun (pkg.inverse_compare pkg'),
+  uniform_continuous_to_fun := uniform_continuous_compare _ _,
+  uniform_continuous_inv_fun := uniform_continuous_compare _ _, }
 
 lemma uniform_continuous_compare_equiv : uniform_continuous (pkg.compare_equiv pkg') :=
 pkg.uniform_continuous_compare pkg'
@@ -253,8 +260,6 @@ protected def prod : abstract_completion (α × β) :=
   dense := pkg.dense.prod_map pkg'.dense }
 end prod
 
-
-
 section extension₂
 variables (pkg' : abstract_completion β)
 local notation `hatβ` := pkg'.space

src/topology/uniform_space/compare_reals.lean

@@ -103,8 +103,8 @@ instance bourbaki.uniform_space: uniform_space Bourbakiℝ := completion.uniform
 /-- Bourbaki reals packaged as a completion of Q using the general theory. -/
 def Bourbaki_pkg : abstract_completion Q := completion.cpkg
 
-/-- The equivalence between Bourbaki and Cauchy reals-/
-noncomputable def compare_equiv : Bourbakiℝ ≃ ℝ :=
+/-- The uniform bijection between Bourbaki and Cauchy reals. -/
+noncomputable def compare_equiv : Bourbakiℝ ≃ᵤ ℝ :=
 Bourbaki_pkg.compare_equiv rational_cau_seq_pkg
 
 lemma compare_uc : uniform_continuous (compare_equiv) :=

src/topology/uniform_space/completion.lean

@@ -407,6 +407,11 @@ lemma dense_inducing_coe : dense_inducing (coe : α → completion α) :=
 { dense := dense_range_coe,
   ..(uniform_inducing_coe α).inducing }
 
+/-- The uniform bijection between a complete space and its uniform completion. -/
+def uniform_completion.complete_equiv_self [complete_space α] [separated_space α]:
+  completion α ≃ᵤ α :=
+abstract_completion.compare_equiv completion.cpkg abstract_completion.of_complete
+
 open topological_space
 
 instance separable_space_completion [separable_space α] : separable_space (completion α) :=