From d45a8ace0fb50f4b0a1ea72bdf57f3881f6f8112 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Wed, 6 Jul 2022 15:08:32 +0000
Subject: [PATCH] refactor(topology/separation): redefine `t0_space` (#15046)

---
 .../prime_spectrum/basic.lean                 |  9 ++-
 src/topology/alexandroff.lean                 | 31 ++++++--
 src/topology/separation.lean                  | 79 ++++++++++---------
 src/topology/uniform_space/separation.lean    |  2 +-
 4 files changed, 70 insertions(+), 51 deletions(-)

diff --git a/src/algebraic_geometry/prime_spectrum/basic.lean b/src/algebraic_geometry/prime_spectrum/basic.lean
index 7ecf5574dbe70..9170666db2a7b 100644
--- a/src/algebraic_geometry/prime_spectrum/basic.lean
+++ b/src/algebraic_geometry/prime_spectrum/basic.lean
@@ -738,9 +738,12 @@ lemma le_iff_specializes (x y : prime_spectrum R) :
   x ≤ y ↔ x ⤳ y :=
 (le_iff_mem_closure x y).trans specializes_iff_mem_closure.symm
 
-instance : t0_space (prime_spectrum R) :=
-by { simp [t0_space_iff_or_not_mem_closure, ← le_iff_mem_closure,
-  ← not_and_distrib, ← le_antisymm_iff, eq_comm] }
+/-- `nhds` as an order embedding. -/
+@[simps { fully_applied := tt }]
+def nhds_order_embedding : prime_spectrum R ↪o filter (prime_spectrum R) :=
+order_embedding.of_map_le_iff nhds $ λ a b, (le_iff_specializes a b).symm
+
+instance : t0_space (prime_spectrum R) := ⟨nhds_order_embedding.injective⟩
 
 end order
 
diff --git a/src/topology/alexandroff.lean b/src/topology/alexandroff.lean
index 5ee52fc4a8df1..adad2ca09f761 100644
--- a/src/topology/alexandroff.lean
+++ b/src/topology/alexandroff.lean
@@ -325,6 +325,26 @@ lemma dense_embedding_coe [noncompact_space X] :
   dense_embedding (coe : X → alexandroff X) :=
 { dense := dense_range_coe, .. open_embedding_coe }
 
+@[simp] lemma specializes_coe {x y : X} : (x : alexandroff X) ⤳ y ↔ x ⤳ y :=
+open_embedding_coe.to_inducing.specializes_iff
+
+@[simp] lemma inseparable_coe {x y : X} : inseparable (x : alexandroff X) y ↔ inseparable x y :=
+open_embedding_coe.to_inducing.inseparable_iff
+
+lemma not_specializes_infty_coe {x : X} : ¬specializes ∞ (x : alexandroff X) :=
+is_closed_infty.not_specializes rfl (coe_ne_infty x)
+
+lemma not_inseparable_infty_coe {x : X} : ¬inseparable ∞ (x : alexandroff X) :=
+λ h, not_specializes_infty_coe h.specializes
+
+lemma not_inseparable_coe_infty {x : X} : ¬inseparable (x : alexandroff X) ∞ :=
+λ h, not_specializes_infty_coe h.specializes'
+
+lemma inseparable_iff {x y : alexandroff X} :
+  inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x' : X, x = x' ∧ ∃ y' : X, y = y' ∧ inseparable x' y' :=
+by induction x using alexandroff.rec; induction y using alexandroff.rec;
+  simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe]
+
 /-!
 ### Compactness and separation properties
 
@@ -351,13 +371,8 @@ instance : compact_space (alexandroff X) :=
 instance [t0_space X] : t0_space (alexandroff X) :=
 begin
   refine ⟨λ x y hxy, _⟩,
-  induction x using alexandroff.rec; induction y using alexandroff.rec,
-  { exact (hxy rfl).elim },
-  { use {∞}ᶜ, simp [is_closed_infty] },
-  { use {∞}ᶜ, simp [is_closed_infty] },
-  { rcases t0_space.t0 x y (mt coe_eq_coe.mpr hxy) with ⟨U, hUo, hU⟩,
-    refine ⟨coe '' U, is_open_image_coe.2 hUo, _⟩,
-    simpa [coe_eq_coe] }
+  rcases inseparable_iff.1 hxy with ⟨rfl, rfl⟩|⟨x, rfl, y, rfl, h⟩,
+  exacts [rfl, congr_arg coe h.eq]
 end
 
 /-- The one point compactification of a `t1_space` space is a `t1_space`. -/
@@ -366,7 +381,7 @@ instance [t1_space X] : t1_space (alexandroff X) :=
   begin
     induction z using alexandroff.rec,
     { exact is_closed_infty },
-    { simp only [← image_singleton, is_closed_image_coe],
+    { rw [← image_singleton, is_closed_image_coe],
       exact ⟨is_closed_singleton, is_compact_singleton⟩ }
   end }
 
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index 13716f00cb9c3..6156350dda142 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -154,29 +154,22 @@ lemma union_right {a b c : set α} (ab : separated a b) (ac : separated a c) :
 
 end separated
 
-/-- A T₀ space, also known as a Kolmogorov space, is a topological space
-  where for every pair `x ≠ y`, there is an open set containing one but not the other. -/
+/-- A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair
+`x ≠ y`, there is an open set containing one but not the other. We formulate the definition in terms
+of the `inseparable` relation.  -/
 class t0_space (α : Type u) [topological_space α] : Prop :=
-(t0 : ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)))
+(t0 : ∀ ⦃x y : α⦄, inseparable x y → x = y)
 
-lemma exists_is_open_xor_mem [t0_space α] {x y : α} (h : x ≠ y) :
-  ∃ U:set α, is_open U ∧ xor (x ∈ U) (y ∈ U) :=
-t0_space.t0 x y h
-
-lemma t0_space_def (α : Type u) [topological_space α] :
-  t0_space α ↔ ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)) :=
-by { split, apply @t0_space.t0, apply t0_space.mk }
+lemma t0_space_iff_inseparable (α : Type u) [topological_space α] :
+  t0_space α ↔ ∀ (x y : α), inseparable x y → x = y :=
+⟨λ ⟨h⟩, h, λ h, ⟨h⟩⟩
 
 lemma t0_space_iff_not_inseparable (α : Type u) [topological_space α] :
   t0_space α ↔ ∀ (x y : α), x ≠ y → ¬inseparable x y :=
-by simp only [t0_space_def, xor_iff_not_iff, not_forall, exists_prop, inseparable_iff_forall_open]
-
-lemma t0_space_iff_inseparable (α : Type u) [topological_space α] :
-  t0_space α ↔ ∀ (x y : α), inseparable x y → x = y :=
-by simp only [t0_space_iff_not_inseparable, ne.def, not_imp_not]
+by simp only [t0_space_iff_inseparable, ne.def, not_imp_not]
 
 lemma inseparable.eq [t0_space α] {x y : α} (h : inseparable x y) : x = y :=
-(t0_space_iff_inseparable α).1 ‹_› x y h
+t0_space.t0 h
 
 lemma t0_space_iff_nhds_injective (α : Type u) [topological_space α] :
   t0_space α ↔ injective (𝓝 : α → filter α) :=
@@ -188,14 +181,23 @@ lemma nhds_injective [t0_space α] : injective (𝓝 : α → filter α) :=
 @[simp] lemma nhds_eq_nhds_iff [t0_space α] {a b : α} : 𝓝 a = 𝓝 b ↔ a = b :=
 nhds_injective.eq_iff
 
+lemma t0_space_iff_exists_is_open_xor_mem (α : Type u) [topological_space α] :
+  t0_space α ↔ ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)) :=
+by simp only [t0_space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop,
+  inseparable_iff_forall_open]
+
+lemma exists_is_open_xor_mem [t0_space α] {x y : α} (h : x ≠ y) :
+  ∃ U : set α, is_open U ∧ xor (x ∈ U) (y ∈ U) :=
+(t0_space_iff_exists_is_open_xor_mem α).1 ‹_› x y h
+
 /-- Specialization forms a partial order on a t0 topological space. -/
 def specialization_order (α : Type*) [topological_space α] [t0_space α] : partial_order α :=
 { .. specialization_preorder α,
   .. partial_order.lift (order_dual.to_dual ∘ 𝓝) nhds_injective }
 
 instance : t0_space (separation_quotient α) :=
-(t0_space_iff_inseparable _).2 $ λ x' y', quotient.induction_on₂' x' y' $
-  λ x y h, separation_quotient.mk_eq_mk.2 $ separation_quotient.inducing_mk.inseparable_iff.1 h
+⟨λ x' y', quotient.induction_on₂' x' y' $
+  λ x y h, separation_quotient.mk_eq_mk.2 $ separation_quotient.inducing_mk.inseparable_iff.1 h⟩
 
 theorem minimal_nonempty_closed_subsingleton [t0_space α] {s : set α} (hs : is_closed s)
   (hmin : ∀ t ⊆ s, t.nonempty → is_closed t → t = s) :
@@ -264,8 +266,7 @@ let ⟨x, _, h⟩ := exists_open_singleton_of_open_finite (finite.of_fintype _)
 
 lemma t0_space_of_injective_of_continuous [topological_space β] {f : α → β}
   (hf : function.injective f) (hf' : continuous f) [t0_space β] : t0_space α :=
-⟨λ x y hxy, let ⟨U, hU, hxyU⟩ := t0_space.t0 (f x) (f y) (hf.ne hxy) in
-  ⟨f ⁻¹' U, hU.preimage hf', hxyU⟩⟩
+⟨λ x y h, hf $ (h.map hf').eq⟩
 
 protected lemma embedding.t0_space [topological_space β] [t0_space β] {f : α → β}
   (hf : embedding f) : t0_space α :=
@@ -279,12 +280,11 @@ theorem t0_space_iff_or_not_mem_closure (α : Type u) [topological_space α] :
 by simp only [t0_space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_distrib]
 
 instance [topological_space β] [t0_space α] [t0_space β] : t0_space (α × β) :=
-(t0_space_iff_inseparable _).2 $
-  λ x y h, prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq
+⟨λ x y h, prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq⟩
 
 instance {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)] [Π i, t0_space (π i)] :
   t0_space (Π i, π i) :=
-(t0_space_iff_inseparable _).2 $ λ x y h, funext $ λ i, (h.map (continuous_apply i)).eq
+⟨λ x y h, funext $ λ i, (h.map (continuous_apply i)).eq⟩
 
 /-- A T₁ space, also known as a Fréchet space, is a topological space
   where every singleton set is closed. Equivalently, for every pair
@@ -367,7 +367,8 @@ lemma t1_space_tfae (α : Type u) [topological_space α] :
     ∀ ⦃x y : α⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
     ∀ ⦃x y : α⦄, x ≠ y → ∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U,
     ∀ ⦃x y : α⦄, x ≠ y → disjoint (𝓝 x) (pure y),
-    ∀ ⦃x y : α⦄, x ≠ y → disjoint (pure x) (𝓝 y)] :=
+    ∀ ⦃x y : α⦄, x ≠ y → disjoint (pure x) (𝓝 y),
+    ∀ ⦃x y : α⦄, x ⤳ y → x = y] :=
 begin
   tfae_have : 1 ↔ 2, from ⟨λ h, h.1, λ h, ⟨h⟩⟩,
   tfae_have : 2 ↔ 3, by simp only [is_open_compl_iff],
@@ -388,6 +389,9 @@ begin
     exacts [is_open_empty, compl_compl s ▸ (@set.finite.is_closed _ _ H _ hs).is_open_compl] },
   tfae_have : 4 → 2,
     from λ h x, (cofinite_topology.is_closed_iff.2 $ or.inr (finite_singleton _)).preimage h,
+  tfae_have : 2 ↔ 10,
+  { simp only [← closure_subset_iff_is_closed, specializes_iff_mem_closure, subset_def,
+      mem_singleton_iff, eq_comm] },
   tfae_finish
 end
 
@@ -408,12 +412,21 @@ lemma t1_space_iff_disjoint_pure_nhds : t1_space α ↔ ∀ ⦃x y : α⦄, x 
 lemma t1_space_iff_disjoint_nhds_pure : t1_space α ↔ ∀ ⦃x y : α⦄, x ≠ y → disjoint (𝓝 x) (pure y) :=
 (t1_space_tfae α).out 0 7
 
+lemma t1_space_iff_specializes_imp_eq : t1_space α ↔ ∀ ⦃x y : α⦄, x ⤳ y → x = y :=
+(t1_space_tfae α).out 0 9
+
 lemma disjoint_pure_nhds [t1_space α] {x y : α} (h : x ≠ y) : disjoint (pure x) (𝓝 y) :=
 t1_space_iff_disjoint_pure_nhds.mp ‹_› h
 
 lemma disjoint_nhds_pure [t1_space α] {x y : α} (h : x ≠ y) : disjoint (𝓝 x) (pure y) :=
 t1_space_iff_disjoint_nhds_pure.mp ‹_› h
 
+lemma specializes.eq [t1_space α] {x y : α} (h : x ⤳ y) : x = y :=
+t1_space_iff_specializes_imp_eq.1 ‹_› h
+
+@[simp] lemma specializes_iff_eq [t1_space α] {x y : α} : x ⤳ y ↔ x = y :=
+⟨specializes.eq, λ h, h ▸ specializes_rfl⟩
+
 instance {α : Type*} : t1_space (cofinite_topology α) :=
 t1_space_iff_continuous_cofinite_of.mpr continuous_id
 
@@ -454,12 +467,7 @@ end
 
 lemma t1_space_of_injective_of_continuous [topological_space β] {f : α → β}
   (hf : function.injective f) (hf' : continuous f) [t1_space β] : t1_space α :=
-{ t1 :=
-  begin
-    intros x,
-    rw [← function.injective.preimage_image hf {x}, image_singleton],
-    exact (t1_space.t1 $ f x).preimage hf'
-  end }
+t1_space_iff_specializes_imp_eq.2 $ λ x y h, hf (h.map hf').eq
 
 protected lemma embedding.t1_space [topological_space β] [t1_space β] {f : α → β}
   (hf : embedding f) : t1_space α :=
@@ -477,8 +485,7 @@ instance {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)] [Π i
 ⟨λ f, univ_pi_singleton f ▸ is_closed_set_pi (λ i hi, is_closed_singleton)⟩
 
 @[priority 100] -- see Note [lower instance priority]
-instance t1_space.t0_space [t1_space α] : t0_space α :=
-⟨λ x y h, ⟨{z | z ≠ y}, is_open_ne, or.inl ⟨h, not_not_intro rfl⟩⟩⟩
+instance t1_space.t0_space [t1_space α] : t0_space α := ⟨λ x y h, h.specializes.eq⟩
 
 @[simp] lemma compl_singleton_mem_nhds_iff [t1_space α] {x y : α} : {x}ᶜ ∈ 𝓝 y ↔ y ≠ x :=
 is_open_compl_singleton.mem_nhds_iff
@@ -498,12 +505,6 @@ hs.induction_on (by simp) $ λ x, by simp
   (closure s).subsingleton ↔ s.subsingleton :=
 ⟨λ h, h.mono subset_closure, λ h, h.closure⟩
 
-lemma specializes.eq [t1_space α] {x y : α} (h : x ⤳ y) : x = y :=
-by simpa only [specializes_iff_mem_closure, closure_singleton, mem_singleton_iff, eq_comm] using h
-
-@[simp] lemma specializes_iff_eq [t1_space α] {x y : α} : x ⤳ y ↔ x = y :=
-⟨specializes.eq, λ h, h ▸ specializes_refl _⟩
-
 lemma is_closed_map_const {α β} [topological_space α] [topological_space β] [t1_space β] {y : β} :
   is_closed_map (function.const α y) :=
 is_closed_map.of_nonempty $ λ s hs h2s, by simp_rw [h2s.image_const, is_closed_singleton]
@@ -1263,7 +1264,7 @@ instance regular_space.t1_space [regular_space α] : t1_space α :=
 begin
   rw t1_space_iff_exists_open,
   intros x y hxy,
-  obtain ⟨U, hU, h⟩ := t0_space.t0 x y hxy,
+  obtain ⟨U, hU, h⟩ := exists_is_open_xor_mem hxy,
   cases h,
   { exact ⟨U, hU, h⟩ },
   { obtain ⟨R, hR, hh⟩ := regular_space.regular (is_closed_compl_iff.mpr hU) (not_not.mpr h.1),
diff --git a/src/topology/uniform_space/separation.lean b/src/topology/uniform_space/separation.lean
index 1de47585c8c59..5249afb7fd724 100644
--- a/src/topology/uniform_space/separation.lean
+++ b/src/topology/uniform_space/separation.lean
@@ -186,7 +186,7 @@ end
 
 @[priority 100] -- see Note [lower instance priority]
 instance separated_regular [separated_space α] : regular_space α :=
-{ t0 := by { haveI := separated_iff_t2.mp ‹_›, exact t1_space.t0_space.t0 },
+{ to_t0_space := by { haveI := separated_iff_t2.mp ‹_›, exact t1_space.t0_space },
   regular := λs a hs ha,
     have sᶜ ∈ 𝓝 a,
       from is_open.mem_nhds hs.is_open_compl ha,