refactor(topology/metric_space/isometry): move material about isometr…

…ies of normed spaces (#8003)

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/topology.20and.20analysis

src/analysis/normed_space/add_torsor.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Yury Kudryashov
 -/
 import linear_algebra.affine_space.midpoint
-import topology.metric_space.isometry
+import analysis.normed_space.basic
 import topology.instances.real_vector_space
 
 /-!

src/analysis/normed_space/basic.lean

@@ -7,7 +7,8 @@ import algebra.punit_instances
 import topology.instances.nnreal
 import topology.algebra.module
 import topology.algebra.algebra
-import topology.metric_space.antilipschitz
+import topology.algebra.group_completion
+import topology.metric_space.completion
 import topology.algebra.ordered.liminf_limsup
 
 /-!
@@ -295,6 +296,55 @@ instance {r : ℝ} : has_neg (sphere (0:α) r) :=
   (((-v) : sphere _ _) : α) = - (v:α) :=
 rfl
 
+namespace isometric
+
+/-- Addition `y ↦ y + x` as an `isometry`. -/
+protected def add_right (x : α) : α ≃ᵢ α :=
+{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_add_right _ _ _,
+  .. equiv.add_right x }
+
+@[simp] lemma add_right_to_equiv (x : α) :
+  (isometric.add_right x).to_equiv = equiv.add_right x := rfl
+
+@[simp] lemma coe_add_right (x : α) : (isometric.add_right x : α → α) = λ y, y + x := rfl
+
+lemma add_right_apply (x y : α) : (isometric.add_right x : α → α) y = y + x := rfl
+
+@[simp] lemma add_right_symm (x : α) :
+  (isometric.add_right x).symm = isometric.add_right (-x) :=
+ext $ λ y, rfl
+
+/-- Addition `y ↦ x + y` as an `isometry`. -/
+protected def add_left (x : α) : α ≃ᵢ α :=
+{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_add_left _ _ _,
+  to_equiv := equiv.add_left x }
+
+@[simp] lemma add_left_to_equiv (x : α) :
+  (isometric.add_left x).to_equiv = equiv.add_left x := rfl
+
+@[simp] lemma coe_add_left (x : α) : ⇑(isometric.add_left x) = (+) x := rfl
+
+@[simp] lemma add_left_symm (x : α) :
+  (isometric.add_left x).symm = isometric.add_left (-x) :=
+ext $ λ y, rfl
+
+variable (α)
+
+/-- Negation `x ↦ -x` as an `isometry`. -/
+protected def neg : α ≃ᵢ α :=
+{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ x y, dist_neg_neg _ _,
+  to_equiv := equiv.neg α }
+
+variable {α}
+
+@[simp] lemma neg_symm : (isometric.neg α).symm = isometric.neg α := rfl
+
+@[simp] lemma neg_to_equiv : (isometric.neg α).to_equiv = equiv.neg α := rfl
+
+@[simp] lemma coe_neg : ⇑(isometric.neg α) = has_neg.neg := rfl
+
+end isometric
+
 theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
   tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε :=
 metric.tendsto_nhds.trans $ by simp only [dist_zero_right]
@@ -372,6 +422,16 @@ begin
   exact ⟨C, λ x hx, hC _ (set.mem_image_of_mem _ hx)⟩,
 end
 
+lemma add_monoid_hom.isometry_iff_norm (f : α →+ β) : isometry f ↔ ∀ x, ∥f x∥ = ∥x∥ :=
+begin
+  simp only [isometry_emetric_iff_metric, dist_eq_norm, ← f.map_sub],
+  refine ⟨λ h x, _, λ h x y, h _⟩,
+  simpa using h x 0
+end
+
+lemma add_monoid_hom.isometry_of_norm (f : α →+ β) (hf : ∀ x, ∥f x∥ = ∥x∥) : isometry f :=
+f.isometry_iff_norm.2 hf
+
 section nnnorm
 
 /-- Version of the norm taking values in nonnegative reals. -/
@@ -1578,6 +1638,14 @@ instance normed_algebra.to_semi_normed_algebra (𝕜 : Type*) (𝕜' : Type*) [n
   [h : semi_normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥ :=
 semi_normed_algebra.norm_algebra_map_eq _
 
+/-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
+lemma algebra_map_isometry (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
+  [semi_normed_algebra 𝕜 𝕜'] : isometry (algebra_map 𝕜 𝕜') :=
+begin
+  refine isometry_emetric_iff_metric.2 (λx y, _),
+  rw [dist_eq_norm, dist_eq_norm, ← ring_hom.map_sub, norm_algebra_map_eq],
+end
+
 variables (𝕜 : Type*) [normed_field 𝕜]
 variables (𝕜' : Type*) [semi_normed_ring 𝕜']
 
@@ -1781,3 +1849,32 @@ lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λa, nnnorm (f
 summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
 
 end summable
+
+namespace uniform_space
+namespace completion
+
+variables (V : Type*)
+
+instance [uniform_space V] [has_norm V] :
+  has_norm (completion V) :=
+{ norm := completion.extension has_norm.norm }
+
+@[simp] lemma norm_coe {V} [semi_normed_group V] (v : V) :
+  ∥(v : completion V)∥ = ∥v∥ :=
+completion.extension_coe uniform_continuous_norm v
+
+instance [semi_normed_group V] : normed_group (completion V) :=
+{ dist_eq :=
+  begin
+    intros x y,
+    apply completion.induction_on₂ x y; clear x y,
+    { refine is_closed_eq (completion.uniform_continuous_extension₂ _).continuous _,
+      exact continuous.comp completion.continuous_extension continuous_sub },
+    { intros x y,
+      rw [← completion.coe_sub, norm_coe, metric.completion.dist_eq, dist_eq_norm] }
+  end,
+  .. (show add_comm_group (completion V), by apply_instance),
+  .. (show metric_space (completion V), by apply_instance) }
+
+end completion
+end uniform_space

src/analysis/normed_space/linear_isometry.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import topology.metric_space.isometry
+import analysis.normed_space.basic
 
 /-!
 # Linear isometries

src/analysis/normed_space/normed_group_hom.lean

@@ -6,7 +6,6 @@ Authors: Johan Commelin
 
 import analysis.normed_space.basic
 import topology.sequences
-import topology.metric_space.isometry
 
 /-!
 # Normed groups homomorphisms

src/topology/algebra/group_completion.lean

@@ -7,6 +7,7 @@ Completion of topological groups:
 -/
 import topology.uniform_space.completion
 import topology.algebra.uniform_group
+
 noncomputable theory
 
 universes u v

src/topology/metric_space/completion.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import topology.uniform_space.completion
 import topology.metric_space.isometry
+import topology.instances.real
 
 /-!
 # The completion of a metric space

src/topology/metric_space/isometry.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Isometries of emetric and metric spaces
 Authors: Sébastien Gouëzel
 -/
-import analysis.normed_space.basic
+import topology.metric_space.antilipschitz
 
 /-!
 # Isometries
@@ -134,22 +134,6 @@ lemma isometry.diam_range [pseudo_metric_space α] [pseudo_metric_space β] {f :
   (hf : isometry f) : metric.diam (range f) = metric.diam (univ : set α) :=
 by { rw ← image_univ, exact hf.diam_image univ }
 
-namespace add_monoid_hom
-
-variables {E F : Type*} [semi_normed_group E] [semi_normed_group F]
-
-lemma isometry_iff_norm (f : E →+ F) : isometry f ↔ ∀ x, ∥f x∥ = ∥x∥ :=
-begin
-  simp only [isometry_emetric_iff_metric, dist_eq_norm, ← f.map_sub],
-  refine ⟨λ h x, _, λ h x y, h _⟩,
-  simpa using h x 0
-end
-
-lemma isometry_of_norm (f : E →+ F) (hf : ∀ x, ∥f x∥ = ∥x∥) : isometry f :=
-f.isometry_iff_norm.2 hf
-
-end add_monoid_hom
-
 /-- `α` and `β` are isometric if there is an isometric bijection between them. -/
 @[nolint has_inhabited_instance] -- such a bijection need not exist
 structure isometric (α : Type*) (β : Type*) [pseudo_emetric_space α] [pseudo_emetric_space β]
@@ -159,6 +143,8 @@ structure isometric (α : Type*) (β : Type*) [pseudo_emetric_space α] [pseudo_
 infix ` ≃ᵢ `:25 := isometric
 
 namespace isometric
+
+section pseudo_emetric_space
 variables [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ]
 
 instance : has_coe_to_fun (α ≃ᵢ β) := ⟨λ_, α → β, λe, e.to_equiv⟩
@@ -304,60 +290,9 @@ lemma mul_apply (e₁ e₂ : α ≃ᵢ α) (x : α) : (e₁ * e₂) x = e₁ (e
 
 @[simp] lemma apply_inv_self (e : α ≃ᵢ α) (x: α) : e (e⁻¹ x) = x := e.apply_symm_apply x
 
-section normed_group
-
-variables {G : Type*} [semi_normed_group G]
-
-/-- Addition `y ↦ y + x` as an `isometry`. -/
-protected def add_right (x : G) : G ≃ᵢ G :=
-{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_add_right _ _ _,
-  .. equiv.add_right x }
-
-@[simp] lemma add_right_to_equiv (x : G) :
-  (isometric.add_right x).to_equiv = equiv.add_right x := rfl
-
-@[simp] lemma coe_add_right (x : G) : (isometric.add_right x : G → G) = λ y, y + x := rfl
-
-lemma add_right_apply (x y : G) : (isometric.add_right x : G → G) y = y + x := rfl
-
-@[simp] lemma add_right_symm (x : G) :
-  (isometric.add_right x).symm = isometric.add_right (-x) :=
-ext $ λ y, rfl
-
-/-- Addition `y ↦ x + y` as an `isometry`. -/
-protected def add_left (x : G) : G ≃ᵢ G :=
-{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_add_left _ _ _,
-  to_equiv := equiv.add_left x }
-
-@[simp] lemma add_left_to_equiv (x : G) :
-  (isometric.add_left x).to_equiv = equiv.add_left x := rfl
+end pseudo_emetric_space
 
-@[simp] lemma coe_add_left (x : G) : ⇑(isometric.add_left x) = (+) x := rfl
-
-@[simp] lemma add_left_symm (x : G) :
-  (isometric.add_left x).symm = isometric.add_left (-x) :=
-ext $ λ y, rfl
-
-variable (G)
-
-/-- Negation `x ↦ -x` as an `isometry`. -/
-protected def neg : G ≃ᵢ G :=
-{ isometry_to_fun := isometry_emetric_iff_metric.2 $ λ x y, dist_neg_neg _ _,
-  to_equiv := equiv.neg G }
-
-variable {G}
-
-@[simp] lemma neg_symm : (isometric.neg G).symm = isometric.neg G := rfl
-
-@[simp] lemma neg_to_equiv : (isometric.neg G).to_equiv = equiv.neg G := rfl
-
-@[simp] lemma coe_neg : ⇑(isometric.neg G) = has_neg.neg := rfl
-
-end normed_group
-
-end isometric
-
-namespace isometric
+section pseudo_metric_space
 
 variables [pseudo_metric_space α] [pseudo_metric_space β] (h : α ≃ᵢ β)
 
@@ -370,6 +305,8 @@ by rw [← image_symm, diam_image]
 lemma diam_univ : metric.diam (univ : set α) = metric.diam (univ : set β) :=
 congr_arg ennreal.to_real h.ediam_univ
 
+end pseudo_metric_space
+
 end isometric
 
 /-- An isometry induces an isometric isomorphism between the source space and the
@@ -382,11 +319,3 @@ def isometry.isometric_on_range [emetric_space α] [pseudo_emetric_space β] {f
 @[simp] lemma isometry.isometric_on_range_apply [emetric_space α] [pseudo_emetric_space β]
   {f : α → β} (h : isometry f) (x : α) : h.isometric_on_range x = ⟨f x, mem_range_self _⟩ :=
 rfl
-
-/-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
-lemma algebra_map_isometry (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
-  [semi_normed_algebra 𝕜 𝕜'] : isometry (algebra_map 𝕜 𝕜') :=
-begin
-  refine isometry_emetric_iff_metric.2 (λx y, _),
-  rw [dist_eq_norm, dist_eq_norm, ← ring_hom.map_sub, norm_algebra_map_eq],
-end