feat(topology/homeomorph): homeo of continuous equivalence from compa…

…ct to T2 (#11072)




Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/topology/homeomorph.lean

@@ -173,11 +173,11 @@ h.embedding.is_compact_iff_is_compact_image.symm
 lemma compact_preimage {s : set β} (h : α ≃ₜ β) : is_compact (h ⁻¹' s) ↔ is_compact s :=
 by rw ← image_symm; exact h.symm.compact_image
 
-lemma compact_space [compact_space α] (h : α ≃ₜ β) : compact_space β :=
+protected lemma compact_space [compact_space α] (h : α ≃ₜ β) : compact_space β :=
 { compact_univ := by { rw [← image_univ_of_surjective h.surjective, h.compact_image],
     apply compact_space.compact_univ } }
 
-lemma t2_space [t2_space α] (h : α ≃ₜ β) : t2_space β :=
+protected lemma t2_space [t2_space α] (h : α ≃ₜ β) : t2_space β :=
 { t2 :=
   begin
     intros x y hxy,
@@ -425,3 +425,70 @@ def image (e : α ≃ₜ β) (s : set α) : s ≃ₜ e '' s :=
   ..e.to_equiv.image s, }
 
 end homeomorph
+
+namespace continuous
+variables [topological_space α] [topological_space β]
+
+lemma continuous_symm_of_equiv_compact_to_t2 [compact_space α] [t2_space β]
+  {f : α ≃ β} (hf : continuous f) : continuous f.symm :=
+begin
+  rw continuous_iff_is_closed,
+  intros C hC,
+  have hC' : is_closed (f '' C) := (hC.is_compact.image hf).is_closed,
+  rwa equiv.image_eq_preimage at hC',
+end
+
+/-- Continuous equivalences from a compact space to a T2 space are homeomorphisms.
+
+This is not true when T2 is weakened to T1
+(see `continuous.homeo_of_equiv_compact_to_t2.t1_counterexample`). -/
+@[simps]
+def homeo_of_equiv_compact_to_t2 [compact_space α] [t2_space β]
+  {f : α ≃ β} (hf : continuous f) : α ≃ₜ β :=
+{ continuous_to_fun := hf,
+  continuous_inv_fun := hf.continuous_symm_of_equiv_compact_to_t2,
+  ..f }
+
+/--
+A concrete counterexample shows that  `continuous.homeo_of_equiv_compact_to_t2`
+cannot be generalized from `t2_space` to `t1_space`.
+
+Let `α = ℕ` be the one-point compactification of `{1, 2, ...}` with the discrete topology,
+where `0` is the adjoined point, and let `β = ℕ` be given the cofinite topology.
+Then `α` is compact, `β` is T1, and the identity map `id : α → β` is a continuous equivalence
+that is not a homeomorphism.
+-/
+lemma homeo_of_equiv_compact_to_t2.t1_counterexample :
+  ∃ (α β : Type) (Iα : topological_space α) (Iβ : topological_space β), by exactI
+  compact_space α ∧ t1_space β ∧ ∃ f : α ≃ β, continuous f ∧ ¬ continuous f.symm :=
+begin
+  /- In the `nhds_adjoint 0 filter.cofinite` topology, a set is open if (1) 0 is not in the set or
+     (2) 0 is in the set and the set is cofinite.  This coincides with the one-point
+     compactification of {1, 2, ...} with the discrete topology. -/
+  let topα : topological_space ℕ := nhds_adjoint 0 filter.cofinite,
+  let topβ : topological_space ℕ := cofinite_topology ℕ,
+  refine ⟨ℕ, ℕ, topα, topβ, _, t1_space_cofinite, equiv.refl ℕ, _, _⟩,
+  { fsplit,
+    rw is_compact_iff_ultrafilter_le_nhds,
+    intros f,
+    suffices : ∃ a, ↑f ≤ @nhds _ topα a, by simpa,
+    by_cases hf : ↑f ≤ @nhds _ topα 0,
+    { exact ⟨0, hf⟩ },
+    { obtain ⟨U, h0U, hU_fin, hUf⟩ : ∃ U : set ℕ, 0 ∈ U ∧ Uᶜ.finite ∧ Uᶜ ∈ f,
+      { rw [nhds_adjoint_nhds, filter.le_def] at hf,
+        push_neg at hf,
+        simpa [and_assoc, ← ultrafilter.compl_mem_iff_not_mem] using hf },
+      obtain ⟨n, hn', hn⟩ := ultrafilter.eq_principal_of_finite_mem hU_fin hUf,
+      rw hn,
+      exact ⟨n, @mem_of_mem_nhds _ topα n⟩ } },
+  { rw continuous_iff_coinduced_le,
+    change topα ≤ topβ,
+    rw gc_nhds,
+    simp [nhds_cofinite] },
+  { intros h,
+    replace h : topβ ≤ topα := by simpa [continuous_iff_coinduced_le, coinduced_id] using h,
+    rw le_nhds_adjoint_iff at h,
+    exact (finite_singleton 1).infinite_compl (h.2 1 one_ne_zero ⟨1, mem_singleton 1⟩) }
+end
+
+end continuous