|
| 1 | +/- |
| 2 | +Copyright (c) 2021 Yury Kudryashov. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Yury Kudryashov |
| 5 | +-/ |
| 6 | +import topology.urysohns_lemma |
| 7 | +import topology.continuous_function.bounded |
| 8 | + |
| 9 | +/-! |
| 10 | +# Metrizability of a normal topological space with second countable topology |
| 11 | +
|
| 12 | +In this file we show that a normal topological space with second countable topology `X` is |
| 13 | +metrizable: there exists a metric space structure that generates the same topology. |
| 14 | +
|
| 15 | +First we prove that `X` can be embedded into `l^∞`, then use this embedding to pull back the metric |
| 16 | +space structure. |
| 17 | +-/ |
| 18 | + |
| 19 | +open set filter metric |
| 20 | +open_locale bounded_continuous_function filter topological_space |
| 21 | + |
| 22 | +namespace topological_space |
| 23 | + |
| 24 | +variables (X : Type*) [topological_space X] [normal_space X] [second_countable_topology X] |
| 25 | + |
| 26 | +/-- A normal topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`. |
| 27 | +-/ |
| 28 | +lemma exists_embedding_l_infty : ∃ f : X → (ℕ →ᵇ ℝ), embedding f := |
| 29 | +begin |
| 30 | + -- Choose a countable basis, and consider the set `s` of pairs of set `(U, V)` such that `U ∈ B`, |
| 31 | + -- `V ∈ B`, and `closure U ⊆ V`. |
| 32 | + rcases exists_countable_basis X with ⟨B, hBc, -, hB⟩, |
| 33 | + set s : set (set X × set X) := {UV ∈ B.prod B| closure UV.1 ⊆ UV.2}, |
| 34 | + -- `s` is a countable set. |
| 35 | + haveI : encodable s := ((hBc.prod hBc).mono (inter_subset_left _ _)).to_encodable, |
| 36 | + -- We don't have the space of bounded (possibly discontinuous) functions, so we equip `s` |
| 37 | + -- with the discrete topology and deal with `s →ᵇ ℝ` instead. |
| 38 | + letI : topological_space s := ⊥, haveI : discrete_topology s := ⟨rfl⟩, |
| 39 | + suffices : ∃ f : X → (s →ᵇ ℝ), embedding f, |
| 40 | + { rcases this with ⟨f, hf⟩, |
| 41 | + exact ⟨λ x, (f x).extend (encodable.encode' s) 0, (bounded_continuous_function.isometry_extend |
| 42 | + (encodable.encode' s) (0 : ℕ →ᵇ ℝ)).embedding.comp hf⟩ }, |
| 43 | + have hd : ∀ UV : s, disjoint (closure UV.1.1) (UV.1.2ᶜ) := |
| 44 | + λ UV, disjoint_compl_right.mono_right (compl_subset_compl.2 UV.2.2), |
| 45 | + -- Choose a sequence of `εₙ > 0`, `n : s`, that is bounded above by `1` and tends to zero |
| 46 | + -- along the `cofinite` filter. |
| 47 | + obtain ⟨ε, ε01, hε⟩ : ∃ ε : s → ℝ, (∀ UV, ε UV ∈ Ioc (0 : ℝ) 1) ∧ tendsto ε cofinite (𝓝 0), |
| 48 | + { rcases pos_sum_of_encodable zero_lt_one s with ⟨ε, ε0, c, hεc, hc1⟩, |
| 49 | + refine ⟨ε, λ UV, ⟨ε0 UV, _⟩, hεc.summable.tendsto_cofinite_zero⟩, |
| 50 | + exact (le_has_sum hεc UV $ λ _ _, (ε0 _).le).trans hc1 }, |
| 51 | + /- For each `UV = (U, V) ∈ s` we use Urysohn's lemma to choose a function `f UV` that is equal to |
| 52 | + zero on `U` and is equal to `ε UV` on the complement to `V`. -/ |
| 53 | + have : ∀ UV : s, ∃ f : C(X, ℝ), eq_on f 0 UV.1.1 ∧ eq_on f (λ _, ε UV) UV.1.2ᶜ ∧ |
| 54 | + ∀ x, f x ∈ Icc 0 (ε UV), |
| 55 | + { intro UV, |
| 56 | + rcases exists_continuous_zero_one_of_closed is_closed_closure |
| 57 | + (hB.is_open UV.2.1.2).is_closed_compl (hd UV) with ⟨f, hf₀, hf₁, hf01⟩, |
| 58 | + exact ⟨ε UV • f, λ x hx, by simp [hf₀ (subset_closure hx)], λ x hx, by simp [hf₁ hx], |
| 59 | + λ x, ⟨mul_nonneg (ε01 _).1.le (hf01 _).1, mul_le_of_le_one_right (ε01 _).1.le (hf01 _).2⟩⟩ }, |
| 60 | + choose f hf0 hfε hf0ε, |
| 61 | + have hf01 : ∀ UV x, f UV x ∈ Icc (0 : ℝ) 1, |
| 62 | + from λ UV x, Icc_subset_Icc_right (ε01 _).2 (hf0ε _ _), |
| 63 | + /- The embedding is given by `F x UV = f UV x`. -/ |
| 64 | + set F : X → s →ᵇ ℝ := λ x, ⟨⟨λ UV, f UV x, continuous_of_discrete_topology⟩, 1, λ UV₁ UV₂, |
| 65 | + real.dist_le_of_mem_Icc_01 (hf01 _ _) (hf01 _ _)⟩, |
| 66 | + have hF : ∀ x UV, F x UV = f UV x := λ _ _, rfl, |
| 67 | + refine ⟨F, embedding.mk' _ (λ x y hxy, _) (λ x, le_antisymm _ _)⟩, |
| 68 | + { /- First we prove that `F` is injective. Indeed, if `F x = F y` and `x ≠ y`, then we can find |
| 69 | + `(U, V) ∈ s` such that `x ∈ U` and `y ∉ V`, hence `F x UV = 0 ≠ ε UV = F y UV`. -/ |
| 70 | + refine not_not.1 (λ Hne, _), -- `by_contra Hne` timeouts |
| 71 | + rcases hB.mem_nhds_iff.1 (is_open_ne.mem_nhds Hne) with ⟨V, hVB, hxV, hVy⟩, |
| 72 | + rcases hB.exists_closure_subset (hB.mem_nhds hVB hxV) with ⟨U, hUB, hxU, hUV⟩, |
| 73 | + set UV : ↥s := ⟨(U, V), ⟨hUB, hVB⟩, hUV⟩, |
| 74 | + apply (ε01 UV).1.ne, |
| 75 | + calc (0 : ℝ) = F x UV : (hf0 UV hxU).symm |
| 76 | + ... = F y UV : by rw hxy |
| 77 | + ... = ε UV : hfε UV (λ h : y ∈ V, hVy h rfl) }, |
| 78 | + { /- Now we prove that each neighborhood `V` of `x : X` include a preimage of a neighborhood of |
| 79 | + `F x` under `F`. Without loss of generality, `V` belongs to `B`. Choose `U ∈ B` such that |
| 80 | + `x ∈ V` and `closure V ⊆ U`. Then the preimage of the `(ε (U, V))`-neighborhood of `F x` |
| 81 | + is included by `V`. -/ |
| 82 | + refine ((nhds_basis_ball.comap _).le_basis_iff hB.nhds_has_basis).2 _, |
| 83 | + rintro V ⟨hVB, hxV⟩, |
| 84 | + rcases hB.exists_closure_subset (hB.mem_nhds hVB hxV) with ⟨U, hUB, hxU, hUV⟩, |
| 85 | + set UV : ↥s := ⟨(U, V), ⟨hUB, hVB⟩, hUV⟩, |
| 86 | + refine ⟨ε UV, (ε01 UV).1, λ y (hy : dist (F y) (F x) < ε UV), _⟩, |
| 87 | + replace hy : dist (F y UV) (F x UV) < ε UV, |
| 88 | + from (bounded_continuous_function.dist_coe_le_dist _).trans_lt hy, |
| 89 | + contrapose! hy, |
| 90 | + rw [hF, hF, hfε UV hy, hf0 UV hxU, pi.zero_apply, dist_zero_right], |
| 91 | + exact le_abs_self _ }, |
| 92 | + { /- Finally, we prove that `F` is continuous. Given `δ > 0`, consider the set `T` of `(U, V) ∈ s` |
| 93 | + such that `ε (U, V) ≥ δ`. Since `ε` tends to zero, `T` is finite. Since each `f` is continuous, |
| 94 | + we can choose a neighborhood such that `dist (F y (U, V)) (F x (U, V)) ≤ δ` for any |
| 95 | + `(U, V) ∈ T`. For `(U, V) ∉ T`, the same inequality is true because both `F y (U, V)` and |
| 96 | + `F x (U, V)` belong to the interval `[0, ε (U, V)]`. -/ |
| 97 | + refine (nhds_basis_closed_ball.comap _).ge_iff.2 (λ δ δ0, _), |
| 98 | + have h_fin : finite {UV : s | δ ≤ ε UV}, by simpa only [← not_lt] using hε (gt_mem_nhds δ0), |
| 99 | + have : ∀ᶠ y in 𝓝 x, ∀ UV, δ ≤ ε UV → dist (F y UV) (F x UV) ≤ δ, |
| 100 | + { refine (eventually_all_finite h_fin).2 (λ UV hUV, _), |
| 101 | + exact (f UV).continuous.tendsto x (closed_ball_mem_nhds _ δ0) }, |
| 102 | + refine this.mono (λ y hy, (bounded_continuous_function.dist_le δ0.le).2 $ λ UV, _), |
| 103 | + cases le_total δ (ε UV) with hle hle, |
| 104 | + exacts [hy _ hle, (real.dist_le_of_mem_Icc (hf0ε _ _) (hf0ε _ _)).trans (by rwa sub_zero)] } |
| 105 | +end |
| 106 | + |
| 107 | +/-- A normal topological space with second countable topology `X` is metrizable: there exists a |
| 108 | +metric space structure that generates the same topology. This definition provides a `metric_space` |
| 109 | +instance such that the corresponding `topological_space X` instance is definitionally equal |
| 110 | +to the original one. -/ |
| 111 | +@[reducible] noncomputable def to_metric_space : metric_space X := |
| 112 | +@metric_space.replace_uniformity X |
| 113 | + ((uniform_space.comap (exists_embedding_l_infty X).some infer_instance).replace_topology |
| 114 | + (exists_embedding_l_infty X).some_spec.induced) |
| 115 | + (metric_space.induced (exists_embedding_l_infty X).some |
| 116 | + (exists_embedding_l_infty X).some_spec.inj infer_instance) |
| 117 | + rfl |
| 118 | + |
| 119 | +end topological_space |
0 commit comments