feat(topology/metric_space/gluing): metric space structure on sigma t…

…ypes (#11965)

We define a (noncanonical) metric space structure on sigma types (aka arbitrary disjoint unions), as follows. Each piece is isometrically embedded in the union, while for `x` and `y` in different pieces their distance is `dist x x0 + 1 + dist y0 y`, where `x0` and `y0` are basepoints in the respective parts. This is *not* registered as an instance.

This definition was already there for sum types (aka disjoint union of two pieces). We also fix this existing definition to avoid `inhabited` assumptions.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/topology/metric_space/gluing.lean

@@ -28,10 +28,11 @@ to this predistance is the desired space.
 This is an instance of a more general construction, where `Φ` and `Ψ` do not have to be isometries,
 but the distances in the image almost coincide, up to `2ε` say. Then one can almost glue the two
 spaces so that the images of a point under `Φ` and `Ψ` are `ε`-close. If `ε > 0`, this yields a
-metric space structure on `X ⊕ Y`, without the need to take a quotient. In particular, when `X`
-and `Y` are inhabited, this gives a natural metric space structure on `X ⊕ Y`, where the basepoints
+metric space structure on `X ⊕ Y`, without the need to take a quotient. In particular,
+this gives a natural metric space structure on `X ⊕ Y`, where the basepoints
 are at distance 1, say, and the distances between other points are obtained by going through the two
 basepoints.
+(We also register the same metric space structure on a general disjoint union `Σ i, E i`).
 
 We also define the inductive limit of metric spaces. Given
 ```
@@ -239,28 +240,28 @@ glues only along the basepoints, putting them at distance 1. We give a direct de
 the distance, without infi, as it is easier to use in applications, and show that it is equal to
 the gluing distance defined above to take advantage of the lemmas we have already proved. -/
 
-
 variables {X : Type u} {Y : Type v} {Z : Type w}
-variables [metric_space X] [metric_space Y] [inhabited X] [inhabited Y]
+variables [metric_space X] [metric_space Y]
 open sum (inl inr)
 
 /-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
 with each factor.
 If the two spaces are bounded, one can say for instance that each point in the first is at distance
 `diam X + diam Y + 1` of each point in the second.
-Instead, we choose a construction that works for unbounded spaces, but requires basepoints.
+Instead, we choose a construction that works for unbounded spaces, but requires basepoints,
+chosen arbitrarily.
 We embed isometrically each factor, set the basepoints at distance 1,
 arbitrarily, and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
 their respective basepoints, plus the distance 1 between the basepoints.
 Since there is an arbitrary choice in this construction, it is not an instance by default. -/
 def sum.dist : X ⊕ Y → X ⊕ Y → ℝ
 | (inl a) (inl a') := dist a a'
 | (inr b) (inr b') := dist b b'
-| (inl a) (inr b)  := dist a default + 1 + dist default b
-| (inr b) (inl a)  := dist b default + 1 + dist default a
+| (inl a) (inr b)  := dist a (nonempty.some ⟨a⟩) + 1 + dist (nonempty.some ⟨b⟩) b
+| (inr b) (inl a)  := dist b (nonempty.some ⟨b⟩) + 1 + dist (nonempty.some ⟨a⟩) a
 
-lemma sum.dist_eq_glue_dist {p q : X ⊕ Y} :
-  sum.dist p q = glue_dist (λ_ : unit, default) (λ_ : unit, default) 1 p q :=
+lemma sum.dist_eq_glue_dist {p q : X ⊕ Y} (x : X) (y : Y) :
+  sum.dist p q = glue_dist (λ _ : unit, nonempty.some ⟨x⟩) (λ _ : unit, nonempty.some ⟨y⟩) 1 p q :=
 by cases p; cases q; refl <|> simp [sum.dist, glue_dist, dist_comm, add_comm, add_left_comm]
 
 private lemma sum.dist_comm (x y : X ⊕ Y) : sum.dist x y = sum.dist y x :=
@@ -298,27 +299,214 @@ def metric_space_sum : metric_space (X ⊕ Y) :=
 { dist               := sum.dist,
   dist_self          := λx, by cases x; simp only [sum.dist, dist_self],
   dist_comm          := sum.dist_comm,
-  dist_triangle      := λp q r,
-    by simp only [dist, sum.dist_eq_glue_dist]; exact glue_dist_triangle _ _ _ (by norm_num) _ _ _,
-  eq_of_dist_eq_zero := λp q,
-    by simp only [dist, sum.dist_eq_glue_dist]; exact glue_eq_of_dist_eq_zero _ _ _ zero_lt_one _ _,
+  dist_triangle      := λ p q r,
+  begin
+    cases p; cases q; cases r,
+    { exact dist_triangle _ _ _ },
+    { simp only [dist, sum.dist_eq_glue_dist p r],
+      exact glue_dist_triangle _ _ _ (by norm_num) _ _ _ },
+    { simp only [dist, sum.dist_eq_glue_dist p q],
+      exact glue_dist_triangle _ _ _ (by norm_num) _ _ _ },
+    { simp only [dist, sum.dist_eq_glue_dist p q],
+      exact glue_dist_triangle _ _ _ (by norm_num) _ _ _ },
+    { simp only [dist, sum.dist_eq_glue_dist q p],
+      exact glue_dist_triangle _ _ _ (by norm_num) _ _ _ },
+    { simp only [dist, sum.dist_eq_glue_dist q p],
+      exact glue_dist_triangle _ _ _ (by norm_num) _ _ _ },
+    { simp only [dist, sum.dist_eq_glue_dist r p],
+      exact glue_dist_triangle _ _ _ (by norm_num) _ _ _ },
+    { exact dist_triangle _ _ _ },
+  end,
+  eq_of_dist_eq_zero := λ p q,
+  begin
+    cases p; cases q,
+    { simp only [sum.dist, dist_eq_zero, imp_self] },
+    { assume h,
+      simp only [dist, sum.dist_eq_glue_dist p q] at h,
+      exact glue_eq_of_dist_eq_zero _ _ _ zero_lt_one _ _ h },
+    { assume h,
+      simp only [dist, sum.dist_eq_glue_dist q p] at h,
+      exact glue_eq_of_dist_eq_zero _ _ _ zero_lt_one _ _ h },
+    { simp only [sum.dist, dist_eq_zero, imp_self] },
+  end,
   to_uniform_space   := sum.uniform_space,
   uniformity_dist    := uniformity_dist_of_mem_uniformity _ _ sum.mem_uniformity }
 
 local attribute [instance] metric_space_sum
 
 lemma sum.dist_eq {x y : X ⊕ Y} : dist x y = sum.dist x y := rfl
 
-/-- The left injection of a space in a disjoint union in an isometry -/
-lemma isometry_on_inl : isometry (sum.inl : X → (X ⊕ Y)) :=
+/-- The left injection of a space in a disjoint union is an isometry -/
+lemma isometry_inl : isometry (sum.inl : X → (X ⊕ Y)) :=
 isometry_emetric_iff_metric.2 $ λx y, rfl
 
-/-- The right injection of a space in a disjoint union in an isometry -/
-lemma isometry_on_inr : isometry (sum.inr : Y → (X ⊕ Y)) :=
+/-- The right injection of a space in a disjoint union is an isometry -/
+lemma isometry_inr : isometry (sum.inr : Y → (X ⊕ Y)) :=
 isometry_emetric_iff_metric.2 $ λx y, rfl
 
 end sum
 
+namespace sigma
+/- Copy of the previous paragraph, but for arbitrary disjoint unions instead of the disjoint union
+of two spaces. I.e., work with sigma types instead of sum types. -/
+
+variables {ι : Type*} {E : ι → Type*} [∀ i, metric_space (E i)]
+
+open_locale classical
+
+/-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
+with each factor.
+We choose a construction that works for unbounded spaces, but requires basepoints,
+chosen arbitrarily.
+We embed isometrically each factor, set the basepoints at distance 1, arbitrarily,
+and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
+their respective basepoints, plus the distance 1 between the basepoints.
+Since there is an arbitrary choice in this construction, it is not an instance by default. -/
+protected def dist : (Σ i, E i) → (Σ i, E i) → ℝ
+| ⟨i, x⟩ ⟨j, y⟩ :=
+    if h : i = j then by { have : E j = E i, by rw h, exact has_dist.dist x (cast this y) }
+    else has_dist.dist x (nonempty.some ⟨x⟩) + 1 + has_dist.dist (nonempty.some ⟨y⟩) y
+
+/-- A `has_dist` instance on the disjoint union `Σ i, E i`.
+We embed isometrically each factor, set the basepoints at distance 1, arbitrarily,
+and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
+their respective basepoints, plus the distance 1 between the basepoints.
+Since there is an arbitrary choice in this construction, it is not an instance by default. -/
+def has_dist : has_dist (Σ i, E i) :=
+⟨sigma.dist⟩
+
+local attribute [instance] sigma.has_dist
+
+@[simp] lemma dist_same (i : ι) (x : E i) (y : E i) :
+  dist (⟨i, x⟩ : Σ j, E j) ⟨i, y⟩ = dist x y :=
+by simp [has_dist.dist, sigma.dist]
+
+@[simp] lemma dist_ne {i j : ι} (h : i ≠ j) (x : E i) (y : E j) :
+  dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ = dist x (nonempty.some ⟨x⟩) + 1 + dist (nonempty.some ⟨y⟩) y :=
+by simp [has_dist.dist, sigma.dist, h]
+
+lemma one_le_dist_of_ne {i j : ι} (h : i ≠ j) (x : E i) (y : E j) :
+  1 ≤ dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ :=
+begin
+  rw sigma.dist_ne h x y,
+  linarith [@dist_nonneg _ _ x (nonempty.some ⟨x⟩), @dist_nonneg _ _ (nonempty.some ⟨y⟩) y]
+end
+
+lemma fst_eq_of_dist_lt_one (x y : Σ i, E i) (h : dist x y < 1) :
+  x.1 = y.1 :=
+begin
+  cases x, cases y,
+  contrapose! h,
+  apply one_le_dist_of_ne h,
+end
+
+protected lemma dist_triangle (x y z : Σ i, E i) :
+  dist x z ≤ dist x y + dist y z :=
+begin
+  rcases x with ⟨i, x⟩, rcases y with ⟨j, y⟩, rcases z with ⟨k, z⟩,
+  rcases eq_or_ne i k with rfl|hik,
+  { rcases eq_or_ne i j with rfl|hij,
+    { simpa using dist_triangle x y z },
+    { simp only [hij, hij.symm, sigma.dist_same, sigma.dist_ne, ne.def, not_false_iff],
+      calc dist x z ≤ dist x (nonempty.some ⟨x⟩) + 0 + 0 + (0 + 0 + dist (nonempty.some ⟨z⟩) z) :
+        by simpa only [zero_add, add_zero] using dist_triangle _ _ _
+      ... ≤ _ : by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one] } },
+  { rcases eq_or_ne i j with rfl|hij,
+    { simp only [hik, sigma.dist_ne, ne.def, not_false_iff, sigma.dist_same],
+      calc dist x (nonempty.some ⟨x⟩) + 1 + dist (nonempty.some ⟨z⟩) z ≤
+        (dist x y + dist y (nonempty.some ⟨y⟩) + 1 + dist (nonempty.some ⟨z⟩) z) :
+          by apply_rules [add_le_add, le_rfl, dist_triangle]
+      ... = _ : by abel },
+    { rcases eq_or_ne j k with rfl|hjk,
+      { simp only [hij, sigma.dist_ne, ne.def, not_false_iff, sigma.dist_same],
+        calc dist x (nonempty.some ⟨x⟩) + 1 + dist (nonempty.some ⟨z⟩) z ≤
+          dist x (nonempty.some ⟨x⟩) + 1 + (dist (nonempty.some ⟨z⟩) y + dist y z) :
+            by apply_rules [add_le_add, le_rfl, dist_triangle]
+        ... = _ : by abel },
+      { simp only [hik, hij, hjk, sigma.dist_ne, ne.def, not_false_iff],
+        calc dist x (nonempty.some ⟨x⟩) + 1 + dist (nonempty.some ⟨z⟩) z
+          = dist x (nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (nonempty.some ⟨z⟩) z) :
+            by simp only [add_zero, zero_add]
+        ... ≤ _ :
+          by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl] } } }
+end
+
+protected lemma is_open_iff (s : set (Σ i, E i)) :
+  is_open s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s :=
+begin
+  split,
+  { rintros hs ⟨i, x⟩ hx,
+    obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ball x ε ⊆ sigma.mk i ⁻¹' s :=
+      metric.is_open_iff.1 (is_open_sigma_iff.1 hs i) x hx,
+    refine ⟨min ε 1, lt_min εpos zero_lt_one, _⟩,
+    rintros ⟨j, y⟩ hy,
+    rcases eq_or_ne i j with rfl|hij,
+    { simp only [sigma.dist_same, lt_min_iff] at hy,
+      exact hε (mem_ball'.2 hy.1) },
+    { apply (lt_irrefl (1 : ℝ) _).elim,
+      calc 1 ≤ sigma.dist ⟨i, x⟩ ⟨j, y⟩ : sigma.one_le_dist_of_ne hij _ _
+      ... < 1 : hy.trans_le (min_le_right _ _) } },
+  { assume H,
+    apply is_open_sigma_iff.2 (λ i, _),
+    apply metric.is_open_iff.2 (λ x hx, _),
+    obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ y, dist (⟨i, x⟩ : Σ j, E j) y < ε → y ∈ s :=
+      H ⟨i, x⟩ hx,
+    refine ⟨ε, εpos, λ y hy, _⟩,
+    apply hε ⟨i, y⟩,
+    rw sigma.dist_same,
+    exact mem_ball'.1 hy }
+end
+
+/-- A metric space structure on the disjoint union `Σ i, E i`.
+We embed isometrically each factor, set the basepoints at distance 1, arbitrarily,
+and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
+their respective basepoints, plus the distance 1 between the basepoints.
+Since there is an arbitrary choice in this construction, it is not an instance by default. -/
+protected def metric_space : metric_space (Σ i, E i) :=
+begin
+  refine metric_space.of_metrizable sigma.dist _ _ sigma.dist_triangle
+    sigma.is_open_iff _,
+  { rintros ⟨i, x⟩, simp [sigma.dist] },
+  { rintros ⟨i, x⟩ ⟨j, y⟩,
+    rcases eq_or_ne i j with rfl|h,
+    { simp [sigma.dist, dist_comm] },
+    { simp only [sigma.dist, dist_comm, h, h.symm, not_false_iff, dif_neg], abel } },
+  { rintros ⟨i, x⟩ ⟨j, y⟩,
+    rcases eq_or_ne i j with rfl|hij,
+    { simp [sigma.dist] },
+    { assume h,
+      apply (lt_irrefl (1 : ℝ) _).elim,
+      calc 1 ≤ sigma.dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ : sigma.one_le_dist_of_ne hij _ _
+      ... < 1 : by { rw h, exact zero_lt_one } } }
+end
+
+local attribute [instance] sigma.metric_space
+
+open_locale topological_space
+open filter
+
+/-- The injection of a space in a disjoint union is an isometry -/
+lemma isometry_mk (i : ι) : isometry (sigma.mk i : E i → Σ k, E k) :=
+isometry_emetric_iff_metric.2 (by simp)
+
+/-- A disjoint union of complete metric spaces is complete. -/
+protected lemma complete_space [∀ i, complete_space (E i)] : complete_space (Σ i, E i) :=
+begin
+  set s : ι → set (Σ i, E i) := λ i, (sigma.fst ⁻¹' {i}),
+  set U := {p : (Σ k, E k) × (Σ k, E k) | dist p.1 p.2 < 1},
+  have hc : ∀ i, is_complete (s i),
+  { intro i,
+    simp only [s, ← range_sigma_mk],
+    exact (isometry_mk i).uniform_inducing.is_complete_range },
+  have hd : ∀ i j (x ∈ s i) (y ∈ s j), (x, y) ∈ U → i = j,
+    from λ i j x hx y hy hxy, (eq.symm hx).trans ((fst_eq_of_dist_lt_one _ _ hxy).trans hy),
+  refine complete_space_of_is_complete_univ _,
+  convert is_complete_Union_separated hc (dist_mem_uniformity zero_lt_one) hd,
+  simp [s, ← preimage_Union]
+end
+
+end sigma
+
 section gluing
 /- Exact gluing of two metric spaces along isometric subsets. -/
 

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -97,7 +97,7 @@ private lemma max_var_bound : dist x y ≤ max_var X Y := calc
     diam_union (mem_image_of_mem _ (mem_univ _)) (mem_image_of_mem _ (mem_univ _))
   ... = diam (univ : set X) + (dist default default + 1 + dist default default) +
           diam (univ : set Y) :
-    by { rw [isometry_on_inl.diam_image, isometry_on_inr.diam_image], refl }
+    by { rw [isometry_inl.diam_image, isometry_inr.diam_image], refl }
   ... = 1 * diam (univ : set X) + 1 + 1 * diam (univ : set Y) : by simp
   ... ≤ 2 * diam (univ : set X) + 1 + 2 * diam (univ : set Y) :
   begin

src/topology/uniform_space/cauchy.lean

@@ -311,6 +311,28 @@ begin
     λ htl, (ht l hl htl).imp $ λ x hx, ⟨or.inr hx.fst, hx.snd⟩⟩
 end
 
+lemma is_complete_Union_separated {ι : Sort*} {s : ι → set α} (hs : ∀ i, is_complete (s i))
+  {U : set (α × α)} (hU : U ∈ 𝓤 α) (hd : ∀ (i j : ι) (x ∈ s i) (y ∈ s j), (x, y) ∈ U → i = j) :
+  is_complete (⋃ i, s i) :=
+begin
+  set S := ⋃ i, s i,
+  intros l hl hls,
+  rw le_principal_iff at hls,
+  casesI cauchy_iff.1 hl with hl_ne hl',
+  obtain ⟨t, htS, htl, htU⟩ : ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U,
+  { rcases hl' U hU with ⟨t, htl, htU⟩,
+    exact ⟨t ∩ S, inter_subset_right _ _, inter_mem htl hls,
+      (set.prod_mono (inter_subset_left _ _) (inter_subset_left _ _)).trans htU⟩ },
+  obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i,
+  { rcases filter.nonempty_of_mem htl with ⟨x, hx⟩,
+    rcases mem_Union.1 (htS hx) with ⟨i, hi⟩,
+    refine ⟨i, λ y hy, _⟩,
+    rcases mem_Union.1 (htS hy) with ⟨j, hj⟩,
+    convert hj, exact hd i j x hi y hj (htU $ mk_mem_prod hx hy) },
+  rcases hs i l hl (le_principal_iff.2 $ mem_of_superset htl hi) with ⟨x, hxs, hlx⟩,
+  exact ⟨x, mem_Union.2 ⟨i, hxs⟩, hlx⟩
+end
+
 /-- A complete space is defined here using uniformities. A uniform space
   is complete if every Cauchy filter converges. -/
 class complete_space (α : Type u) [uniform_space α] : Prop :=