feat(topology/uniform/uniform_embedding): a sum of two complete space…

…s is complete (#11971)




Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

src/topology/uniform_space/basic.lean

@@ -274,8 +274,8 @@ uniform_space_eq rfl
 
 /-- Replace topology in a `uniform_space` instance with a propositionally (but possibly not
 definitionally) equal one. -/
-def uniform_space.replace_topology {α : Type*} [i : topological_space α] (u : uniform_space α)
-  (h : i = u.to_topological_space) : uniform_space α :=
+@[reducible] def uniform_space.replace_topology {α : Type*} [i : topological_space α]
+  (u : uniform_space α) (h : i = u.to_topological_space) : uniform_space α :=
 uniform_space.of_core_eq u.to_core i $ h.trans u.to_core_to_topological_space.symm
 
 lemma uniform_space.replace_topology_eq {α : Type*} [i : topological_space α] (u : uniform_space α)
@@ -1129,6 +1129,12 @@ lemma to_topological_space_inf {u v : uniform_space α} :
   (u ⊓ v).to_topological_space = u.to_topological_space ⊓ v.to_topological_space :=
 by rw [to_topological_space_Inf, infi_pair]
 
+/-- A uniform space with the discrete uniformity has the discrete topology. -/
+lemma discrete_topology_of_discrete_uniformity [hα : uniform_space α]
+  (h : uniformity α = 𝓟 id_rel) :
+  discrete_topology α :=
+⟨(uniform_space_eq h.symm : ⊥ = hα) ▸ rfl⟩
+
 instance : uniform_space empty := ⊥
 instance : uniform_space punit := ⊥
 instance : uniform_space bool := ⊥

src/topology/uniform_space/uniform_embedding.lean

@@ -90,6 +90,36 @@ by simp only [uniform_embedding_def, uniform_continuous_def]; exact
  λ ⟨I, H₁, H₂⟩, ⟨I, λ s, ⟨H₂ s,
    λ ⟨t, tu, h⟩, mem_of_superset (H₁ t tu) (λ ⟨a, b⟩, h a b)⟩⟩⟩
 
+theorem uniform_embedding_inl : uniform_embedding (sum.inl : α → α ⊕ β) :=
+begin
+  apply uniform_embedding_def.2 ⟨sum.inl_injective, λ s, ⟨_, _⟩⟩,
+  { assume hs,
+    refine ⟨(λ p : α × α, (sum.inl p.1, sum.inl p.2)) '' s ∪
+      (λ p : β × β, (sum.inr p.1, sum.inr p.2)) '' univ, _, _⟩,
+    { exact union_mem_uniformity_sum hs univ_mem },
+    { simp } },
+  { rintros ⟨t, ht, h't⟩,
+    simp only [sum.uniformity, mem_sup, mem_map] at ht,
+    apply filter.mem_of_superset ht.1,
+    rintros ⟨x, y⟩ hx,
+    exact h't _ _ hx }
+end
+
+theorem uniform_embedding_inr : uniform_embedding (sum.inr : β → α ⊕ β) :=
+begin
+  apply uniform_embedding_def.2 ⟨sum.inr_injective, λ s, ⟨_, _⟩⟩,
+  { assume hs,
+    refine ⟨(λ p : α × α, (sum.inl p.1, sum.inl p.2)) '' univ ∪
+      (λ p : β × β, (sum.inr p.1, sum.inr p.2)) '' s, _, _⟩,
+    { exact union_mem_uniformity_sum univ_mem hs },
+    { simp } },
+  { rintros ⟨t, ht, h't⟩,
+    simp only [sum.uniformity, mem_sup, mem_map] at ht,
+    apply filter.mem_of_superset ht.2,
+    rintros ⟨x, y⟩ hx,
+    exact h't _ _ hx }
+end
+
 /-- If the domain of a `uniform_inducing` map `f` is a `separated_space`, then `f` is injective,
 hence it is a `uniform_embedding`. -/
 protected theorem uniform_inducing.uniform_embedding [separated_space α] {f : α → β}
@@ -355,13 +385,40 @@ lemma totally_bounded_preimage {f : α → β} {s : set β} (hf : uniform_embedd
   exact ⟨y, zc, ts (by exact zt)⟩
 end
 
+instance complete_space.sum [complete_space α] [complete_space β] :
+  complete_space (α ⊕ β) :=
+begin
+  rw complete_space_iff_is_complete_univ,
+  have A : is_complete (range (sum.inl : α → α ⊕ β)) :=
+    uniform_embedding_inl.to_uniform_inducing.is_complete_range,
+  have B : is_complete (range (sum.inr : β → α ⊕ β)) :=
+    uniform_embedding_inr.to_uniform_inducing.is_complete_range,
+  convert A.union B,
+  apply (eq_univ_of_forall (λ x, _)).symm,
+  cases x,
+  { left, exact mem_range_self _ },
+  { right, exact mem_range_self _ }
+end
+
 end
 
 lemma uniform_embedding_comap {α : Type*} {β : Type*} {f : α → β} [u : uniform_space β]
   (hf : function.injective f) : @uniform_embedding α β (uniform_space.comap f u) u f :=
 @uniform_embedding.mk _ _ (uniform_space.comap f u) _ _
   (@uniform_inducing.mk _ _ (uniform_space.comap f u) _ _ rfl) hf
 
+/-- Pull back a uniform space structure by an embedding, adjusting the new uniform structure to
+make sure that its topology is defeq to the original one. -/
+def embedding.comap_uniform_space {α β} [topological_space α] [u : uniform_space β] (f : α → β)
+  (h : embedding f) : uniform_space α :=
+(u.comap f).replace_topology h.induced
+
+lemma embedding.to_uniform_embedding {α β} [topological_space α] [u : uniform_space β] (f : α → β)
+  (h : embedding f) :
+  @uniform_embedding α β (h.comap_uniform_space f) u f :=
+{ comap_uniformity := rfl,
+  inj := h.inj }
+
 section uniform_extension
 
 variables {α : Type*} {β : Type*} {γ : Type*}