feat(topology/subset_properties, noetherian_space): Noetherian spaces…

… have finite irreducible components. (#17015)

The previous statement was too weak.



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/topology/noetherian_space.lean

@@ -206,28 +206,25 @@ begin
 end
 
 lemma noetherian_space.finite_irreducible_components [noetherian_space α] :
-  (set.range irreducible_component : set (set α)).finite :=
+  (irreducible_components α).finite :=
 begin
   classical,
   obtain ⟨S, hS₁, hS₂⟩ := noetherian_space.exists_finset_irreducible (⊤ : closeds α),
-  suffices : ∀ x : α, ∃ s : S, irreducible_component x = s,
-  { choose f hf,
-    rw [show irreducible_component = coe ∘ f, from funext hf, set.range_comp],
-    exact (set.finite.intro infer_instance).image _ },
-  intro x,
-  obtain ⟨z, hz, hz'⟩ : ∃ (z : set α) (H : z ∈ finset.image coe S), irreducible_component x ⊆ z,
+  suffices : irreducible_components α ⊆ coe '' (S : set $ closeds α),
+  { exact set.finite.subset ((set.finite.intro infer_instance).image _) this },
+  intros K hK,
+  obtain ⟨z, hz, hz'⟩ : ∃ (z : set α) (H : z ∈ finset.image coe S), K ⊆ z,
   { convert is_irreducible_iff_sUnion_closed.mp
-      is_irreducible_irreducible_component (S.image coe) _ _,
-    { apply_instance },
+      hK.1 (S.image coe) _ _,
     { simp only [finset.mem_image, exists_prop, forall_exists_index, and_imp],
       rintro _ z hz rfl,
       exact z.2 },
     { exact (set.subset_univ _).trans ((congr_arg coe hS₂).trans $ by simp).subset } },
   obtain ⟨s, hs, e⟩ := finset.mem_image.mp hz,
   rw ← e at hz',
-  use ⟨s, hs⟩,
+  refine ⟨s, hs, _⟩,
   symmetry,
-  apply eq_irreducible_component (hS₁ _).2,
+  suffices : K ≤ s, { exact this.antisymm (hK.2 (hS₁ ⟨s, hs⟩) this) },
   simpa,
 end
 

src/topology/subset_properties.lean

@@ -9,6 +9,7 @@ import data.finset.order
 import data.set.accumulate
 import tactic.tfae
 import topology.bornology.basic
+import order.minimal
 
 /-!
 # Properties of subsets of topological spaces
@@ -1580,6 +1581,29 @@ let ⟨m, hm, hsm, hmm⟩ := zorn_subset_nonempty {t : set α | is_preirreducibl
     λ x hxc, subset_sUnion_of_mem hxc⟩) s H in
 ⟨m, hm, hsm, λ u hu hmu, hmm _ hu hmu⟩
 
+/-- The set of irreducible components of a topological space. -/
+def irreducible_components (α : Type*) [topological_space α] : set (set α) :=
+maximals (≤) { s : set α | is_irreducible s }
+
+lemma is_closed_of_mem_irreducible_components (s ∈ irreducible_components α) :
+  is_closed s :=
+begin
+  rw [← closure_eq_iff_is_closed, eq_comm],
+  exact subset_closure.antisymm (H.2 H.1.closure subset_closure),
+end
+
+lemma irreducible_components_eq_maximals_closed (α : Type*) [topological_space α] :
+  irreducible_components α = maximals (≤) { s : set α | is_closed s ∧ is_irreducible s } :=
+begin
+  ext s,
+  split,
+  { intro H, exact ⟨⟨is_closed_of_mem_irreducible_components _ H, H.1⟩, λ x h e, H.2 h.2 e⟩ },
+  { intro H, refine ⟨H.1.2, λ x h e, _⟩,
+    have : closure x ≤ s,
+    { exact H.2 ⟨is_closed_closure, h.closure⟩ (e.trans subset_closure) },
+    exact le_trans subset_closure this }
+end
+
 /-- A maximal irreducible set that contains a given point. -/
 def irreducible_component (x : α) : set α :=
 classical.some (exists_preirreducible {x} is_irreducible_singleton.is_preirreducible)
@@ -1599,11 +1623,13 @@ theorem eq_irreducible_component {x : α} :
   ∀ {s : set α}, is_preirreducible s → irreducible_component x ⊆ s → s = irreducible_component x :=
 (irreducible_component_property x).2.2
 
+lemma irreducible_component_mem_irreducible_components (x : α) :
+  irreducible_component x ∈ irreducible_components α :=
+⟨is_irreducible_irreducible_component, λ s h₁ h₂,(eq_irreducible_component h₁.2 h₂).le⟩
+
 theorem is_closed_irreducible_component {x : α} :
   is_closed (irreducible_component x) :=
-closure_eq_iff_is_closed.1 $ eq_irreducible_component
-  is_irreducible_irreducible_component.is_preirreducible.closure
-  subset_closure
+is_closed_of_mem_irreducible_components _ (irreducible_component_mem_irreducible_components x)
 
 /-- A preirreducible space is one where there is no non-trivial pair of disjoint opens. -/
 class preirreducible_space (α : Type u) [topological_space α] : Prop :=

src/topology/uniform_space/compact.lean

@@ -80,7 +80,7 @@ def uniform_space_of_compact_t2 [topological_space γ] [compact_space γ] [t2_sp
   end,
   symm := begin
     refine le_of_eq _,
-    rw map_supr,
+    rw filter.map_supr,
     congr' with x : 1,
     erw [nhds_prod_eq, ← prod_comm],
   end,
@@ -184,7 +184,7 @@ lemma compact_space.uniform_continuous_of_continuous [compact_space α]
   {f : α → β} (h : continuous f) : uniform_continuous f :=
 calc
 map (prod.map f f) (𝓤 α) = map (prod.map f f) (⨆ x, 𝓝 (x, x))  : by rw compact_space_uniformity
-                     ... =  ⨆ x, map (prod.map f f) (𝓝 (x, x)) : by rw map_supr
+                     ... =  ⨆ x, map (prod.map f f) (𝓝 (x, x)) : by rw filter.map_supr
                      ... ≤ ⨆ x, 𝓝 (f x, f x)     : supr_mono (λ x, (h.prod_map h).continuous_at)
                      ... ≤ ⨆ y, 𝓝 (y, y)         : supr_comp_le (λ y, 𝓝 (y, y)) f
                      ... ≤ 𝓤 β                   : supr_nhds_le_uniformity