feat(Topology): embedding a countably separated space inside a space of sequences (#30849)

Author: FormulaRabbit81

Mathlib/Topology/MetricSpace/PiNat.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
+import Mathlib.Analysis.Normed.Group.FunctionSeries
 import Mathlib.Topology.Algebra.MetricSpace.Lipschitz
 import Mathlib.Topology.MetricSpace.HausdorffDistance
 
@@ -46,6 +47,10 @@ in general), and `ι` is countable.
     `dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i))`.
 * `PiCountable.metricSpace` is the corresponding metric space structure, adjusted so that
   the uniformity is definitionally the product uniformity. Not registered as an instance.
+* `PiNatEmbed` gives an equivalence between a space and itself in a sequence of spaces
+* `Metric.PiNatEmbed.metricSpace` proves that a topological `X` separated by countably many
+  continuous functions to metric spaces, can be embedded inside their product.
+
 -/
 
 noncomputable section
@@ -757,14 +762,15 @@ theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type*) [Metr
     simpa only [nonempty_coe_sort] using g_surj.nonempty
   exact ⟨g ∘ f, g_cont.comp f_cont, g_surj.comp f_surj⟩
 
+open Encodable ENNReal
 namespace PiCountable
 
 /-!
 ### Products of (possibly non-discrete) metric spaces
 -/
 
 variable {ι : Type*} [Encodable ι] {F : ι → Type*}
-open Encodable ENNReal
+
 section EDist
 variable [∀ i, EDist (F i)] {x y : ∀ i, F i} {i : ι} {r : ℝ≥0∞}
 
@@ -934,3 +940,142 @@ protected def metricSpace : MetricSpace (∀ i, F i) :=
 
 end MetricSpace
 end PiCountable
+
+/-! ### Embedding a countably separated space inside a space of sequences -/
+
+namespace Metric
+
+open scoped PiCountable
+
+variable {ι X : Type*} {Y : ι → Type*} {f : ∀ i, X → Y i}
+
+include f in
+variable (X Y f) in
+/-- Given a type `X` and a sequence `Y` of metric spaces and a sequence `f : : ∀ i, X → Y i` of
+separating functions, `PiNatEmbed X Y f` is a type synonym for `X` seen as a subset of `∀ i, Y i`.
+-/
+structure PiNatEmbed (X : Type*) (Y : ι → Type*) (f : ∀ i, X → Y i) where
+  /-- The map from `X` to the subset of `∀ i, Y i`. -/
+  toPiNat ::
+  /-- The map from the subset of `∀ i, Y i` to `X`. -/
+  ofPiNat : X
+
+namespace PiNatEmbed
+
+@[ext] lemma ext {x y : PiNatEmbed X Y f} (hxy : x.ofPiNat = y.ofPiNat) : x = y := by
+  cases x; congr!
+
+variable (X Y f) in
+/-- Equivalence between `X` and its embedding into `∀ i, Y i`. -/
+@[simps]
+def toPiNatEquiv : X ≃ PiNatEmbed X Y f where
+  toFun := toPiNat
+  invFun := ofPiNat
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp] lemma ofPiNat_inj {x y : PiNatEmbed X Y f} :  x.ofPiNat = y.ofPiNat ↔ x = y :=
+  (toPiNatEquiv X Y f).symm.injective.eq_iff
+
+@[simp] lemma «forall» {P : PiNatEmbed X Y f → Prop} : (∀ x, P x) ↔ ∀ x, P (toPiNat x) :=
+  (toPiNatEquiv X Y f).symm.forall_congr_left
+
+variable (X Y f) in
+/-- `X` equipped with the distance coming from `∀ i, Y i` embeds in `∀ i, Y i`. -/
+noncomputable def embed : PiNatEmbed X Y f → ∀ i, Y i := fun x i ↦ f i x.ofPiNat
+
+lemma embed_injective (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    Injective (embed X Y f) := by
+  simpa [Pairwise, not_imp_comm (a := _ = _), funext_iff, Function.Injective] using separating_f
+
+variable [Encodable ι]
+
+section PseudoEMetricSpace
+variable [∀ i, PseudoEMetricSpace (Y i)]
+
+noncomputable instance : PseudoEMetricSpace (PiNatEmbed X Y f) :=
+  .induced (embed X Y f) PiCountable.pseudoEMetricSpace
+
+lemma edist_def (x y : PiNatEmbed X Y f) :
+    edist x y = ∑' i, min (2⁻¹ ^ encode i) (edist (f i x.ofPiNat) (f i y.ofPiNat)) := rfl
+
+lemma isometry_embed : Isometry (embed X Y f) := PseudoEMetricSpace.isometry_induced _
+
+end PseudoEMetricSpace
+
+section PseudoMetricSpace
+variable [∀ i, PseudoMetricSpace (Y i)]
+
+noncomputable instance : PseudoMetricSpace (PiNatEmbed X Y f) :=
+  .induced (embed X Y f) PiCountable.pseudoMetricSpace
+
+lemma dist_def (x y : PiNatEmbed X Y f) :
+    dist x y = ∑' i, min (2⁻¹ ^ encode i) (dist (f i x.ofPiNat) (f i y.ofPiNat)) := rfl
+
+variable [TopologicalSpace X]
+
+lemma continuous_toPiNat (continuous_f : ∀ i, Continuous (f i)) :
+    Continuous (toPiNat : X → PiNatEmbed X Y f) := by
+  rw [continuous_iff_continuous_dist]
+  simp only [dist_def]
+  apply continuous_tsum (by fun_prop) summable_geometric_two_encode <| by simp [abs_of_nonneg]
+
+end PseudoMetricSpace
+
+section EMetricSpace
+variable [∀ i, EMetricSpace (Y i)]
+
+/-- If the functions `f i : X → Y i` separate points of `X`, then `X` can be embedded into
+`∀ i, Y i`. -/
+noncomputable abbrev emetricSpace (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    EMetricSpace (PiNatEmbed X Y f) :=
+  .induced (embed X Y f) (embed_injective separating_f) PiCountable.emetricSpace
+
+lemma isUniformEmbedding_embed (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    IsUniformEmbedding (embed X Y f) :=
+  let := emetricSpace separating_f; isometry_embed.isUniformEmbedding
+
+end EMetricSpace
+
+
+section MetricSpace
+variable [∀ i, MetricSpace (Y i)]
+
+/-- If the functions `f i : X → Y i` separate points of `X`, then `X` can be embedded into
+`∀ i, Y i`. -/
+noncomputable abbrev metricSpace (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    MetricSpace (PiNatEmbed X Y f) :=
+  (emetricSpace separating_f).toMetricSpace fun x y ↦ by simp [edist_dist]
+
+section CompactSpace
+variable [TopologicalSpace X] [CompactSpace X]
+
+lemma isHomeomorph_toPiNat (continuous_f : ∀ i, Continuous (f i))
+    (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    IsHomeomorph (toPiNat : X → PiNatEmbed X Y f) := by
+  letI := emetricSpace separating_f
+  rw [isHomeomorph_iff_continuous_bijective]
+  exact ⟨continuous_toPiNat continuous_f, (toPiNatEquiv X Y f).bijective⟩
+
+variable (X Y f) in
+/-- Homeomorphism between `X` and its embedding into `∀ i, Y i` induced by a separating family of
+continuous functions `f i : X → Y i`. -/
+@[simps!]
+noncomputable def toPiNatHomeo (continuous_f : ∀ i, Continuous (f i))
+    (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    X ≃ₜ PiNatEmbed X Y f :=
+  (toPiNatEquiv X Y f).toHomeomorphOfIsInducing
+    (isHomeomorph_toPiNat continuous_f separating_f).isInducing
+
+/-- If `X` is compact, and there exists a sequence of continuous functions `f i : X → Y i` to
+metric spaces `Y i` that separate points on `X`, then `X` is metrizable. -/
+lemma TopologicalSpace.MetrizableSpace.of_countable_separating (f : ∀ i, X → Y i)
+    (continuous_f : ∀ i, Continuous (f i)) (separating_f : Pairwise fun x y ↦ ∃ i, f i x ≠ f i y) :
+    MetrizableSpace X :=
+  letI := Metric.PiNatEmbed.metricSpace separating_f
+  (Metric.PiNatEmbed.toPiNatHomeo X Y f continuous_f separating_f).isEmbedding.metrizableSpace
+
+end CompactSpace
+end MetricSpace
+end PiNatEmbed
+end Metric