From 322bfd98fe3949adb8ec22a4f6659081d003f6d8 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 24 Jan 2024 17:22:13 -0600 Subject: [PATCH 1/3] feat: link `Isometry` to `Dilation` --- Mathlib/Topology/MetricSpace/Dilation.lean | 17 ++++++++++- .../Topology/MetricSpace/DilationEquiv.lean | 28 +++++++++++++++++++ 2 files changed, 44 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/MetricSpace/Dilation.lean b/Mathlib/Topology/MetricSpace/Dilation.lean index ac384132ec0f7..c7235763c7551 100644 --- a/Mathlib/Topology/MetricSpace/Dilation.lean +++ b/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 diff --git a/Mathlib/Topology/MetricSpace/DilationEquiv.lean b/Mathlib/Topology/MetricSpace/DilationEquiv.lean index 59a5c956f4b20..e2583701b7d3c 100644 --- a/Mathlib/Topology/MetricSpace/DilationEquiv.lean +++ b/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,32 @@ 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] + end PseudoEMetricSpace section PseudoMetricSpace From 89ff880bfbb81e8618c494f14a33aed952d37bd4 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 24 Jan 2024 17:37:12 -0600 Subject: [PATCH 2/3] add `Homeomorph` --- Mathlib/Topology/MetricSpace/DilationEquiv.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Mathlib/Topology/MetricSpace/DilationEquiv.lean b/Mathlib/Topology/MetricSpace/DilationEquiv.lean index e2583701b7d3c..c28cdce117d71 100644 --- a/Mathlib/Topology/MetricSpace/DilationEquiv.lean +++ b/Mathlib/Topology/MetricSpace/DilationEquiv.lean @@ -204,6 +204,20 @@ lemma _root_.IsometryEquiv.toDilationEquiv_toDilation (e : X ≃ᵢ Y) : 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 From 5e4dd8ff4ddb4206318a1ac40f9451061b5f679f Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 25 Jan 2024 16:21:51 -0600 Subject: [PATCH 3/3] make `f` explicit --- Mathlib/Topology/MetricSpace/Dilation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/MetricSpace/Dilation.lean b/Mathlib/Topology/MetricSpace/Dilation.lean index c7235763c7551..5e48af60ffa65 100644 --- a/Mathlib/Topology/MetricSpace/Dilation.lean +++ b/Mathlib/Topology/MetricSpace/Dilation.lean @@ -267,7 +267,7 @@ 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 +def _root_.Isometry.toDilation (f : α → β) (hf : Isometry f) : α →ᵈ β where toFun := f edist_eq' := ⟨1, one_ne_zero, by simpa using hf⟩