feat: port Topology.Sober (#2134)

Mathlib.lean

@@ -1034,6 +1034,7 @@ import Mathlib.Topology.Paracompact
 import Mathlib.Topology.Perfect
 import Mathlib.Topology.Separation
 import Mathlib.Topology.ShrinkingLemma
+import Mathlib.Topology.Sober
 import Mathlib.Topology.SubsetProperties
 import Mathlib.Topology.Support
 import Mathlib.Topology.UniformSpace.AbsoluteValue

Mathlib/Topology/Basic.lean

@@ -1756,6 +1756,13 @@ theorem image_closure_subset_closure_image {f : α → β} {s : Set α} (h : Con
   ((mapsTo_image f s).closure h).image_subset
 #align image_closure_subset_closure_image image_closure_subset_closure_image
 
+-- porting note: new lemma
+theorem closure_image_closure {f : α → β} {s : Set α} (h : Continuous f) :
+    closure (f '' closure s) = closure (f '' s) :=
+  Subset.antisymm
+    (closure_minimal (image_closure_subset_closure_image h) isClosed_closure)
+    (closure_mono <| image_subset _ subset_closure)
+
 theorem closure_subset_preimage_closure_image {f : α → β} {s : Set α} (h : Continuous f) :
     closure s ⊆ f ⁻¹' closure (f '' s) := by
   rw [← Set.image_subset_iff]

Mathlib/Topology/Sober.lean

@@ -0,0 +1,253 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+
+! This file was ported from Lean 3 source module topology.sober
+! leanprover-community/mathlib commit 0a0ec35061ed9960bf0e7ffb0335f44447b58977
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Separation
+
+/-!
+# Sober spaces
+
+A quasi-sober space is a topological space where every
+irreducible closed subset has a generic point.
+A sober space is a quasi-sober space where every irreducible closed subset
+has a *unique* generic point. This is if and only if the space is T0, and thus sober spaces can be
+stated via `[QuasiSober α] [T0Space α]`.
+
+## Main definition
+
+* `IsGenericPoint` : `x` is the generic point of `S` if `S` is the closure of `x`.
+* `QuasiSober` : A space is quasi-sober if every irreducible closed subset has a generic point.
+
+-/
+
+
+open Set
+
+variable {α β : Type _} [TopologicalSpace α] [TopologicalSpace β]
+
+section genericPoint
+
+/-- `x` is a generic point of `S` if `S` is the closure of `x`. -/
+def IsGenericPoint (x : α) (S : Set α) : Prop :=
+  closure ({x} : Set α) = S
+#align is_generic_point IsGenericPoint
+
+theorem isGenericPoint_def {x : α} {S : Set α} : IsGenericPoint x S ↔ closure ({x} : Set α) = S :=
+  Iff.rfl
+#align is_generic_point_def isGenericPoint_def
+
+theorem IsGenericPoint.def {x : α} {S : Set α} (h : IsGenericPoint x S) :
+    closure ({x} : Set α) = S :=
+  h
+#align is_generic_point.def IsGenericPoint.def
+
+theorem isGenericPoint_closure {x : α} : IsGenericPoint x (closure ({x} : Set α)) :=
+  refl _
+#align is_generic_point_closure isGenericPoint_closure
+
+variable {x y : α} {S U Z : Set α}
+
+theorem isGenericPoint_iff_specializes : IsGenericPoint x S ↔ ∀ y, x ⤳ y ↔ y ∈ S := by
+  simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]
+#align is_generic_point_iff_specializes isGenericPoint_iff_specializes
+
+namespace IsGenericPoint
+
+theorem specializes_iff_mem (h : IsGenericPoint x S) : x ⤳ y ↔ y ∈ S :=
+  isGenericPoint_iff_specializes.1 h y
+#align is_generic_point.specializes_iff_mem IsGenericPoint.specializes_iff_mem
+
+protected theorem specializes (h : IsGenericPoint x S) (h' : y ∈ S) : x ⤳ y :=
+  h.specializes_iff_mem.2 h'
+#align is_generic_point.specializes IsGenericPoint.specializes
+
+protected theorem mem (h : IsGenericPoint x S) : x ∈ S :=
+  h.specializes_iff_mem.1 specializes_rfl
+#align is_generic_point.mem IsGenericPoint.mem
+
+protected theorem isClosed (h : IsGenericPoint x S) : IsClosed S :=
+  h.def ▸ isClosed_closure
+#align is_generic_point.is_closed IsGenericPoint.isClosed
+
+protected theorem isIrreducible (h : IsGenericPoint x S) : IsIrreducible S :=
+  h.def ▸ isIrreducible_singleton.closure
+#align is_generic_point.is_irreducible IsGenericPoint.isIrreducible
+
+protected theorem inseparable (h : IsGenericPoint x S) (h' : IsGenericPoint y S) :
+    Inseparable x y :=
+  (h.specializes h'.mem).antisymm (h'.specializes h.mem)
+
+/-- In a T₀ space, each set has at most one generic point. -/
+protected theorem eq [T0Space α] (h : IsGenericPoint x S) (h' : IsGenericPoint y S) : x = y :=
+  (h.inseparable h').eq
+#align is_generic_point.eq IsGenericPoint.eq
+
+theorem mem_open_set_iff (h : IsGenericPoint x S) (hU : IsOpen U) : x ∈ U ↔ (S ∩ U).Nonempty :=
+  ⟨fun h' => ⟨x, h.mem, h'⟩, fun ⟨_y, hyS, hyU⟩ => (h.specializes hyS).mem_open hU hyU⟩
+#align is_generic_point.mem_open_set_iff IsGenericPoint.mem_open_set_iff
+
+theorem disjoint_iff (h : IsGenericPoint x S) (hU : IsOpen U) : Disjoint S U ↔ x ∉ U := by
+  rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]
+#align is_generic_point.disjoint_iff IsGenericPoint.disjoint_iff
+
+theorem mem_closed_set_iff (h : IsGenericPoint x S) (hZ : IsClosed Z) : x ∈ Z ↔ S ⊆ Z := by
+  rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]
+#align is_generic_point.mem_closed_set_iff IsGenericPoint.mem_closed_set_iff
+
+protected theorem image (h : IsGenericPoint x S) {f : α → β} (hf : Continuous f) :
+    IsGenericPoint (f x) (closure (f '' S)) := by
+  rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
+#align is_generic_point.image IsGenericPoint.image
+
+end IsGenericPoint
+
+theorem isGenericPoint_iff_forall_closed (hS : IsClosed S) (hxS : x ∈ S) :
+    IsGenericPoint x S ↔ ∀ Z : Set α, IsClosed Z → x ∈ Z → S ⊆ Z := by
+  have : closure {x} ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS
+  simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and_iff, closure, subset_interₛ_iff,
+    mem_setOf_eq, and_imp, singleton_subset_iff]
+#align is_generic_point_iff_forall_closed isGenericPoint_iff_forall_closed
+
+end genericPoint
+
+section Sober
+
+/-- A space is sober if every irreducible closed subset has a generic point. -/
+@[mk_iff quasiSober_iff]
+class QuasiSober (α : Type _) [TopologicalSpace α] : Prop where
+  sober : ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
+#align quasi_sober QuasiSober
+
+/-- A generic point of the closure of an irreducible space. -/
+noncomputable def IsIrreducible.genericPoint [QuasiSober α] {S : Set α} (hS : IsIrreducible S) :
+    α :=
+  (QuasiSober.sober hS.closure isClosed_closure).choose
+#align is_irreducible.generic_point IsIrreducible.genericPoint
+
+theorem IsIrreducible.genericPoint_spec [QuasiSober α] {S : Set α} (hS : IsIrreducible S) :
+    IsGenericPoint hS.genericPoint (closure S) :=
+  (QuasiSober.sober hS.closure isClosed_closure).choose_spec
+#align is_irreducible.generic_point_spec IsIrreducible.genericPoint_spec
+
+@[simp]
+theorem IsIrreducible.genericPoint_closure_eq [QuasiSober α] {S : Set α} (hS : IsIrreducible S) :
+    closure ({hS.genericPoint} : Set α) = closure S :=
+  hS.genericPoint_spec
+#align is_irreducible.generic_point_closure_eq IsIrreducible.genericPoint_closure_eq
+
+variable (α)
+
+/-- A generic point of a sober irreducible space. -/
+noncomputable def genericPoint [QuasiSober α] [IrreducibleSpace α] : α :=
+  (IrreducibleSpace.isIrreducible_univ α).genericPoint
+#align generic_point genericPoint
+
+theorem genericPoint_spec [QuasiSober α] [IrreducibleSpace α] : IsGenericPoint (genericPoint α) ⊤ :=
+  by simpa using (IrreducibleSpace.isIrreducible_univ α).genericPoint_spec
+#align generic_point_spec genericPoint_spec
+
+@[simp]
+theorem genericPoint_closure [QuasiSober α] [IrreducibleSpace α] :
+    closure ({genericPoint α} : Set α) = ⊤ :=
+  genericPoint_spec α
+#align generic_point_closure genericPoint_closure
+
+variable {α}
+
+theorem genericPoint_specializes [QuasiSober α] [IrreducibleSpace α] (x : α) : genericPoint α ⤳ x :=
+  (IsIrreducible.genericPoint_spec _).specializes (by simp)
+#align generic_point_specializes genericPoint_specializes
+
+attribute [local instance] specializationOrder
+
+/-- The closed irreducible subsets of a sober space bijects with the points of the space. -/
+noncomputable def irreducibleSetEquivPoints [QuasiSober α] [T0Space α] :
+    { s : Set α | IsIrreducible s ∧ IsClosed s } ≃o α where
+  toFun s := s.prop.1.genericPoint
+  invFun x := ⟨closure ({x} : Set α), isIrreducible_singleton.closure, isClosed_closure⟩
+  left_inv s := Subtype.eq <| Eq.trans s.prop.1.genericPoint_spec <|
+    closure_eq_iff_isClosed.mpr s.2.2
+  right_inv x := isIrreducible_singleton.closure.genericPoint_spec.eq
+      (by rw [closure_closure]; exact isGenericPoint_closure)
+  map_rel_iff' := by
+    rintro ⟨s, hs⟩ ⟨t, ht⟩
+    refine specializes_iff_closure_subset.trans ?_
+    simp [hs.2.closure_eq, ht.2.closure_eq]
+#align irreducible_set_equiv_points irreducibleSetEquivPoints
+
+theorem ClosedEmbedding.quasiSober {f : α → β} (hf : ClosedEmbedding f) [QuasiSober β] :
+    QuasiSober α where
+  sober hS hS' := by
+    have hS'' := hS.image f hf.continuous.continuousOn
+    obtain ⟨x, hx⟩ := QuasiSober.sober hS'' (hf.isClosedMap _ hS')
+    obtain ⟨y, -, rfl⟩ := hx.mem
+    use y
+    apply image_injective.mpr hf.inj
+    rw [← hx.def, ← hf.closure_image_eq, image_singleton]
+#align closed_embedding.quasi_sober ClosedEmbedding.quasiSober
+
+theorem OpenEmbedding.quasiSober {f : α → β} (hf : OpenEmbedding f) [QuasiSober β] :
+    QuasiSober α where
+  sober hS hS' := by
+    have hS'' := hS.image f hf.continuous.continuousOn
+    obtain ⟨x, hx⟩ := QuasiSober.sober hS''.closure isClosed_closure
+    obtain ⟨T, hT, rfl⟩ := hf.toInducing.isClosed_iff.mp hS'
+    rw [image_preimage_eq_inter_range] at hx hS''
+    have hxT : x ∈ T := by
+      rw [← hT.closure_eq]
+      exact closure_mono (inter_subset_left _ _) hx.mem
+    obtain ⟨y, rfl⟩ : x ∈ range f := by
+      rw [hx.mem_open_set_iff hf.open_range]
+      refine' Nonempty.mono _ hS''.1
+      simpa using subset_closure
+    use y
+    change _ = _
+    rw [hf.toEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx]
+    apply image_injective.mpr hf.inj
+    ext z
+    simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff]
+    exact fun hy => ⟨fun h => hT.closure_eq ▸ closure_mono (inter_subset_left _ _) h,
+      fun h => subset_closure ⟨h, hy⟩⟩
+#align open_embedding.quasi_sober OpenEmbedding.quasiSober
+
+/-- A space is quasi sober if it can be covered by open quasi sober subsets. -/
+theorem quasiSober_of_open_cover (S : Set (Set α)) (hS : ∀ s : S, IsOpen (s : Set α))
+    [hS' : ∀ s : S, QuasiSober s] (hS'' : ⋃₀ S = ⊤) : QuasiSober α := by
+  rw [quasiSober_iff]
+  intro t h h'
+  obtain ⟨x, hx⟩ := h.1
+  obtain ⟨U, hU, hU'⟩ : x ∈ ⋃₀ S := by
+    rw [hS'']
+    trivial
+  haveI : QuasiSober U := hS' ⟨U, hU⟩
+  have H : IsPreirreducible ((↑) ⁻¹' t : Set U) :=
+    h.2.preimage (hS ⟨U, hU⟩).openEmbedding_subtype_val
+  replace H : IsIrreducible ((↑) ⁻¹' t : Set U) := ⟨⟨⟨x, hU'⟩, by simpa using hx⟩, H⟩
+  use H.genericPoint
+  have := continuous_subtype_val.closure_preimage_subset _ H.genericPoint_spec.mem
+  rw [h'.closure_eq] at this
+  apply le_antisymm
+  · apply h'.closure_subset_iff.mpr
+    simpa using this
+  rw [← image_singleton, ← closure_image_closure continuous_subtype_val, H.genericPoint_spec.def]
+  refine' (subset_closure_inter_of_isPreirreducible_of_isOpen h.2 (hS ⟨U, hU⟩) ⟨x, hx, hU'⟩).trans
+    (closure_mono _)
+  rw [← Subtype.image_preimage_coe]
+  exact Set.image_subset _ subset_closure
+#align quasi_sober_of_open_cover quasiSober_of_open_cover
+
+/-- Any Hausdorff space is a quasi-sober space because any irreducible set is a singleton. -/
+instance (priority := 100) T2Space.quasiSober [T2Space α] : QuasiSober α where
+  sober h _ := by
+    obtain ⟨x, rfl⟩ := isIrreducible_iff_singleton.mp h
+    exact ⟨x, closure_singleton⟩
+#align t2_space.quasi_sober T2Space.quasiSober
+
+end Sober
+

Mathlib/Topology/SubsetProperties.lean

@@ -1667,17 +1667,23 @@ theorem isPreirreducible_iff_closure {s : Set α} :
     IsPreirreducible (closure s) ↔ IsPreirreducible s :=
   forall₄_congr fun u v hu hv => by
     iterate 3 rw [closure_inter_open_nonempty_iff]
-    exacts[hu.inter hv, hv, hu]
+    exacts [hu.inter hv, hv, hu]
 #align is_preirreducible_iff_closure isPreirreducible_iff_closure
 
 theorem isIrreducible_iff_closure {s : Set α} : IsIrreducible (closure s) ↔ IsIrreducible s :=
   and_congr closure_nonempty_iff isPreirreducible_iff_closure
 #align is_irreducible_iff_closure isIrreducible_iff_closure
 
-alias isPreirreducible_iff_closure ↔ _ IsPreirreducible.closure
+-- porting note: todo: use `alias` + `@[protected]`
+protected lemma IsPreirreducible.closure {s : Set α} (h : IsPreirreducible s) :
+    IsPreirreducible (closure s) :=
+  isPreirreducible_iff_closure.2 h
 #align is_preirreducible.closure IsPreirreducible.closure
 
-alias isIrreducible_iff_closure ↔ _ IsIrreducible.closure
+-- porting note: todo: use `alias` + `@[protected]`
+protected lemma IsIrreducible.closure {s : Set α} (h : IsIrreducible s) :
+    IsIrreducible (closure s) :=
+  isIrreducible_iff_closure.2 h
 #align is_irreducible.closure IsIrreducible.closure
 
 theorem exists_preirreducible (s : Set α) (H : IsPreirreducible s) :