feat: link Dilation to Isometry and Homeomorph (#9980)

Mathlib/Topology/MetricSpace/Dilation.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Dilations of emetric and metric spaces
 Authors: Hanting Zhang
 -/
-import Mathlib.Topology.MetricSpace.Lipschitz
 import Mathlib.Topology.MetricSpace.Antilipschitz
+import Mathlib.Topology.MetricSpace.Isometry
+import Mathlib.Topology.MetricSpace.Lipschitz
 import Mathlib.Data.FunLike.Basic
 
 #align_import topology.metric_space.dilation from "leanprover-community/mathlib"@"93f880918cb51905fd51b76add8273cbc27718ab"
@@ -264,6 +265,20 @@ variable [DilationClass F α β] [DilationClass G β γ]
 
 variable (f : F) (g : G) {x y z : α} {s : Set α}
 
+/-- Every isometry is a dilation of ratio `1`. -/
+@[simps]
+def _root_.Isometry.toDilation (f : α → β) (hf : Isometry f) : α →ᵈ β where
+  toFun := f
+  edist_eq' := ⟨1, one_ne_zero, by simpa using hf⟩
+
+@[simp]
+lemma _root_.Isometry.toDilation_ratio {f : α → β} {hf : Isometry f} : ratio hf.toDilation = 1 := by
+  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
+  · exact ratio_of_trivial hf.toDilation h
+  · push_neg at h
+    obtain ⟨x, y, h₁, h₂⟩ := h
+    exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm
+
 theorem lipschitz : LipschitzWith (ratio f) (f : α → β) := fun x y => (edist_eq f x y).le
 #align dilation.lipschitz Dilation.lipschitz
 

Mathlib/Topology/MetricSpace/DilationEquiv.lean

@@ -89,6 +89,8 @@ def Simps.symm_apply (e : X ≃ᵈ Y) : Y → X := e.symm
 
 initialize_simps_projections DilationEquiv (toFun → apply, invFun → symm_apply)
 
+lemma ratio_toDilation (e : X ≃ᵈ Y) : ratio e.toDilation = ratio e := rfl
+
 /-- Identity map as a `DilationEquiv`. -/
 @[simps! (config := .asFn) apply]
 def refl (X : Type*) [PseudoEMetricSpace X] : X ≃ᵈ X where
@@ -176,6 +178,46 @@ def toPerm : (X ≃ᵈ X) →* Equiv.Perm X where
 theorem coe_pow (e : X ≃ᵈ X) (n : ℕ) : ⇑(e ^ n) = e^[n] := by
   rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]; rfl
 
+-- TODO: Once `IsometryEquiv` follows the `*EquivClass` pattern, replace this with an instance
+-- of `DilationEquivClass` assuming `IsometryEquivClass`.
+/-- Every isometry equivalence is a dilation equivalence of ratio `1`. -/
+def _root_.IsometryEquiv.toDilationEquiv (e : X ≃ᵢ Y) : X ≃ᵈ Y where
+  edist_eq' := ⟨1, one_ne_zero, by simpa using e.isometry⟩
+  __ := e.toEquiv
+
+@[simp]
+lemma _root_.IsometryEquiv.toDilationEquiv_apply (e : X ≃ᵢ Y) (x : X) :
+    e.toDilationEquiv x = e x :=
+  rfl
+
+@[simp]
+lemma _root_.IsometryEquiv.toDilationEquiv_symm (e : X ≃ᵢ Y) :
+    e.toDilationEquiv.symm = e.symm.toDilationEquiv :=
+  rfl
+
+@[simp]
+lemma _root_.IsometryEquiv.toDilationEquiv_toDilation (e : X ≃ᵢ Y) :
+    (e.toDilationEquiv.toDilation : X →ᵈ Y) = e.isometry.toDilation :=
+  rfl
+
+@[simp]
+lemma _root_.IsometryEquiv.toDilationEquiv_ratio (e : X ≃ᵢ Y) : ratio e.toDilationEquiv = 1 := by
+  rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]
+
+/-- Reinterpret a `DilationEquiv` as a homeomorphism. -/
+def toHomeomorph (e : X ≃ᵈ Y) : X ≃ₜ Y where
+  continuous_toFun := Dilation.toContinuous e
+  continuous_invFun := Dilation.toContinuous e.symm
+  __ := e.toEquiv
+
+@[simp]
+lemma coe_toHomeomorph (e : X ≃ᵈ Y) : ⇑e.toHomeomorph = e :=
+  rfl
+
+@[simp]
+lemma toHomeomorph_symm (e : X ≃ᵈ Y) : e.toHomeomorph.symm = e.symm.toHomeomorph :=
+  rfl
+
 end PseudoEMetricSpace
 
 section PseudoMetricSpace