feat(topology/perfect): Schemes, embedding of the Cantor space (#18248)

Felix-Weilacher · Felix-Weilacher · commit 49b7f94aab3a · 2023-04-17T20:49:23.000Z
Add to `topology.perfect` the following theorem: In a complete metric space, any nonempty perfect set admits a continuous embedding of the Cantor space.

The proof uses an object which in descriptive set theory is sometimes called a "scheme". Some attempt was made to include in `topology.metric_space.cantor_scheme` a general theory of these schemes, since they should be useful down the line in other results as well.

We also define `pi_nat.res` in `topology.metric_space.pi_nat`.
diff --git a/src/topology/metric_space/cantor_scheme.lean b/src/topology/metric_space/cantor_scheme.lean
@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2023 Felix Weilacher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Felix Weilacher
+-/
+import topology.metric_space.pi_nat
+
+/-!
+# (Topological) Schemes and their induced maps
+
+In topology, and especially descriptive set theory, one often constructs functions `(ℕ → β) → α`,
+where α is some topological space and β is a discrete space, as an appropriate limit of some map
+`list β → set α`. We call the latter type of map a "`β`-scheme on `α`".
+
+This file develops the basic, abstract theory of these schemes and the functions they induce.
+
+## Main Definitions
+
+* `cantor_scheme.induced_map A` : The aforementioned "limit" of a scheme `A : list β → set α`.
+  This is a partial function from `ℕ → β` to `a`,
+  implemented here as an object of type `Σ s : set (ℕ → β), s → α`.
+  That is, `(induced_map A).1` is the domain and `(induced_map A).2` is the function.
+
+## Implementation Notes
+
+We consider end-appending to be the fundamental way to build lists (say on `β`) inductively,
+as this interacts better with the topology on `ℕ → β`.
+As a result, functions like `list.nth` or `stream.take` do not have their intended meaning
+in this file. See instead `pi_nat.res`.
+
+## References
+
+* [kechris1995] (Chapters 6-7)
+
+## Tags
+
+scheme, cantor scheme, lusin scheme, approximation.
+
+-/
+
+namespace cantor_scheme
+
+open list function filter set pi_nat
+open_locale classical topology
+
+variables {β α : Type*} (A : list β → set α)
+
+/-- From a `β`-scheme on `α` `A`, we define a partial function from `(ℕ → β)` to `α`
+which sends each infinite sequence `x` to an element of the intersection along the
+branch corresponding to `x`, if it exists.
+We call this the map induced by the scheme. -/
+noncomputable def induced_map : Σ s : set (ℕ → β), s → α :=
+⟨λ x, set.nonempty ⋂ n : ℕ, A (res x n), λ x, x.property.some⟩
+
+section topology
+
+/-- A scheme is antitone if each set contains its children. -/
+protected def antitone : Prop := ∀ l : list β, ∀ a : β, A (a :: l) ⊆ A l
+
+/-- A useful strengthening of being antitone is to require that each set contains
+the closure of each of its children. -/
+def closure_antitone [topological_space α] : Prop :=
+∀ l : list β, ∀ a : β, closure (A (a :: l)) ⊆ A l
+
+/-- A scheme is disjoint if the children of each set of pairwise disjoint. -/
+protected def disjoint : Prop :=
+∀ l : list β, _root_.pairwise $ λ a b, disjoint (A (a :: l)) (A (b :: l))
+
+variable {A}
+
+/-- If `x` is in the domain of the induced map of a scheme `A`,
+its image under this map is in each set along the corresponding branch. -/
+lemma map_mem (x : (induced_map A).1) (n : ℕ) :
+  (induced_map A).2 x ∈ A (res x n) :=
+begin
+  have := x.property.some_mem,
+  rw mem_Inter at this,
+  exact this n,
+end
+
+protected lemma closure_antitone.antitone [topological_space α] (hA : closure_antitone A) :
+  cantor_scheme.antitone A :=
+λ l a, subset_closure.trans (hA l a)
+
+protected lemma antitone.closure_antitone [topological_space α] (hanti : cantor_scheme.antitone A)
+  (hclosed : ∀ l, is_closed (A l)) : closure_antitone A :=
+λ l a, (hclosed _).closure_eq.subset.trans (hanti _ _)
+
+/-- A scheme where the children of each set are pairwise disjoint induces an injective map. -/
+theorem disjoint.map_injective (hA : cantor_scheme.disjoint A) : injective (induced_map A).2 :=
+begin
+  rintros ⟨x, hx⟩ ⟨y, hy⟩ hxy,
+  refine subtype.coe_injective (res_injective _),
+  dsimp,
+  ext n : 1,
+  induction n with n ih, { simp },
+  simp only [res_succ],
+  refine ⟨_, ih⟩,
+  contrapose hA,
+  simp only [cantor_scheme.disjoint, _root_.pairwise, ne.def, not_forall, exists_prop],
+  refine ⟨res x n, _, _, hA, _⟩,
+  rw not_disjoint_iff,
+  refine ⟨(induced_map A).2 ⟨x, hx⟩, _, _⟩,
+  { rw ← res_succ,
+    apply map_mem, },
+  rw [hxy, ih, ← res_succ],
+  apply map_mem,
+end
+
+end topology
+
+section metric
+
+variable [pseudo_metric_space α]
+
+variable (A)
+
+/-- A scheme on a metric space has vanishing diameter if diameter approaches 0 along each branch. -/
+def vanishing_diam : Prop :=
+∀ x : ℕ → β, tendsto (λ n : ℕ, emetric.diam (A (res x n))) at_top (𝓝 0)
+
+variable {A}
+
+lemma vanishing_diam.dist_lt (hA : vanishing_diam A) (ε : ℝ) (ε_pos : 0 < ε) (x : ℕ → β) :
+  ∃ n : ℕ, ∀ y z ∈ A (res x n), dist y z < ε :=
+begin
+  specialize hA x,
+  rw ennreal.tendsto_at_top_zero at hA,
+  cases hA (ennreal.of_real (ε / 2))
+    (by { simp only [gt_iff_lt, ennreal.of_real_pos], linarith }) with n hn,
+  use n,
+  intros y hy z hz,
+  rw [← ennreal.of_real_lt_of_real_iff ε_pos, ← edist_dist],
+  apply lt_of_le_of_lt (emetric.edist_le_diam_of_mem hy hz),
+  apply lt_of_le_of_lt (hn _ (le_refl _)),
+  rw ennreal.of_real_lt_of_real_iff ε_pos,
+  linarith,
+end
+
+/-- A scheme with vanishing diameter along each branch induces a continuous map. -/
+theorem vanishing_diam.map_continuous [topological_space β] [discrete_topology β]
+  (hA : vanishing_diam A) : continuous (induced_map A).2 :=
+begin
+  rw metric.continuous_iff',
+  rintros ⟨x, hx⟩ ε ε_pos,
+  cases hA.dist_lt _ ε_pos x with n hn,
+  rw _root_.eventually_nhds_iff,
+  refine ⟨coe ⁻¹' cylinder x n, _, _, by simp⟩,
+  { rintros ⟨y, hy⟩ hyx,
+    rw [mem_preimage, subtype.coe_mk, cylinder_eq_res, mem_set_of] at hyx,
+    apply hn,
+    { rw ← hyx,
+      apply map_mem, },
+    apply map_mem, },
+  apply continuous_subtype_coe.is_open_preimage,
+  apply is_open_cylinder,
+end
+
+/-- A scheme on a complete space with vanishing diameter
+such that each set contains the closure of its children
+induces a total map. -/
+theorem closure_antitone.map_of_vanishing_diam [complete_space α]
+  (hdiam : vanishing_diam A) (hanti : closure_antitone A) (hnonempty : ∀ l, (A l).nonempty) :
+  (induced_map A).1 = univ :=
+begin
+  rw eq_univ_iff_forall,
+  intro x,
+  choose u hu using λ n, hnonempty (res x n),
+  have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n),
+  { have : antitone (λ n : ℕ, A (res x n)),
+    { refine antitone_nat_of_succ_le _,
+      intro n,
+      apply hanti.antitone, },
+    intros n m hnm,
+    exact this hnm (hu _), },
+  have : cauchy_seq u,
+  { rw metric.cauchy_seq_iff,
+    intros ε ε_pos,
+    cases hdiam.dist_lt _ ε_pos x with n hn,
+    use n,
+    intros m₀ hm₀ m₁ hm₁,
+    apply hn; apply umem; assumption, },
+  cases cauchy_seq_tendsto_of_complete this with y hy,
+  use y,
+  rw mem_Inter,
+  intro n,
+  apply hanti _ (x n),
+  apply mem_closure_of_tendsto hy,
+  rw eventually_at_top,
+  exact ⟨n.succ, umem _⟩,
+end
+
+end metric
+
+end cantor_scheme
diff --git a/src/topology/metric_space/pi_nat.lean b/src/topology/metric_space/pi_nat.lean
@@ -196,6 +196,60 @@ lemma update_mem_cylinder (x : Π n, E n) (n : ℕ) (y : E n) :
   update x n y ∈ cylinder x n :=
 mem_cylinder_iff.2 (λ i hi, by simp [hi.ne])
 
+section res
+
+variable {α : Type*}
+open list
+
+/-- In the case where `E` has constant value `α`,
+the cylinder `cylinder x n` can be identified with the element of `list α`
+consisting of the first `n` entries of `x`. See `cylinder_eq_res`.
+We call this list `res x n`, the restriction of `x` to `n`.-/
+def res (x : ℕ → α) : ℕ → list α
+| 0            := nil
+| (nat.succ n) := x n :: res n
+
+@[simp] lemma res_zero (x : ℕ → α) : res x 0 = @nil α := rfl
+@[simp] lemma res_succ (x : ℕ → α) (n : ℕ) : res x n.succ = x n :: res x n := rfl
+
+@[simp] lemma res_length (x : ℕ → α) (n : ℕ) : (res x n).length = n :=
+by induction n; simp [*]
+
+/-- The restrictions of `x` and `y` to `n` are equal if and only if `x m = y m` for all `m < n`.-/
+lemma res_eq_res {x y : ℕ → α} {n : ℕ} : res x n = res y n ↔ ∀ ⦃m⦄, m < n → x m = y m :=
+begin
+  split; intro h; induction n with n ih, { simp },
+  { intros m hm,
+    rw nat.lt_succ_iff_lt_or_eq at hm,
+    simp only [res_succ] at h,
+    cases hm with hm hm,
+    { exact ih h.2 hm },
+    rw hm,
+    exact h.1, },
+  { simp },
+  simp only [res_succ],
+  refine ⟨h (nat.lt_succ_self _), ih (λ m hm, _)⟩,
+  exact h (hm.trans (nat.lt_succ_self _)),
+end
+
+lemma res_injective : injective (@res α) :=
+begin
+  intros x y h,
+  ext n,
+  apply (res_eq_res).mp _ (nat.lt_succ_self _),
+  rw h,
+end
+
+/-- `cylinder x n` is equal to the set of sequences `y` with the same restriction to `n` as `x`.-/
+theorem cylinder_eq_res (x : ℕ → α) (n : ℕ) : cylinder x n = {y | res y n = res x n} :=
+begin
+  ext y,
+  dsimp [cylinder],
+  rw res_eq_res,
+end
+
+end res
+
 /-!
 ### A distance function on `Π n, E n`
 
@@ -305,13 +359,18 @@ end
 
 variables (E) [∀ n, topological_space (E n)] [∀ n, discrete_topology (E n)]
 
-lemma is_topological_basis_cylinders  :
+lemma is_open_cylinder (x : Π n, E n) (n : ℕ) : is_open (cylinder x n) :=
+begin
+  rw pi_nat.cylinder_eq_pi,
+  exact is_open_set_pi (finset.range n).finite_to_set (λ a ha, is_open_discrete _),
+end
+
+lemma is_topological_basis_cylinders :
   is_topological_basis {s : set (Π n, E n) | ∃ (x : Π n, E n) (n : ℕ), s = cylinder x n} :=
 begin
   apply is_topological_basis_of_open_of_nhds,
   { rintros u ⟨x, n, rfl⟩,
-    rw cylinder_eq_pi,
-    exact is_open_set_pi (finset.range n).finite_to_set (λ a ha, is_open_discrete _) },
+    apply is_open_cylinder, },
   { assume x u hx u_open,
     obtain ⟨v, ⟨U, F, hUF, rfl⟩, xU, Uu⟩ : ∃ (v : set (Π (i : ℕ), E i))
       (H : v ∈ {S : set (Π (i : ℕ), E i) | ∃ (U : Π (i : ℕ), set (E i)) (F : finset ℕ),
diff --git a/src/topology/perfect.lean b/src/topology/perfect.lean
