From 535162c482ed03da42660c444c479ec9f704d3d9 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 12 Mar 2026 15:02:24 +0000
Subject: [PATCH 1/9] feat(Topology/SpectralSpace/WLocal/Basic): prove basic
 w-local space lemmas

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../Topology/SpectralSpace/WLocal/Basic.lean  | 92 +++++++++++++++++--
 1 file changed, 83 insertions(+), 9 deletions(-)

diff --git a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
index 8982bad..57d8723 100644
--- a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
+++ b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
@@ -5,7 +5,7 @@ Authors: Jiedong Jiang, Christian Merten
 -/
 import Proetale.Mathlib.Topology.Inseparable
 import Proetale.Mathlib.Topology.Separation.Basic
-import Mathlib.Topology.Spectral.Basic
+import Proetale.Mathlib.Topology.Spectral.Basic
 import Mathlib.Topology.JacobsonSpace
 
 /-!
@@ -34,28 +34,102 @@ attribute [instance] WLocalSpace.isClosed_closedPoints
 @[mk_iff]
 structure IsWLocalMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop
     extends IsSpectralMap f where
-  preimage_closedPoints : f ⁻¹' (closedPoints Y) ⊆ closedPoints X
+  image_closedPoints : closedPoints X ⊆ f ⁻¹' (closedPoints Y)
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
 lemma IsWLocalMap.comp {Z : Type*} [TopologicalSpace Z] {f : X → Y} {g : Y → Z}
     (hf : IsWLocalMap f) (hg : IsWLocalMap g) :
-    IsWLocalMap (g ∘ f) :=
-  sorry
+    IsWLocalMap (g ∘ f) where
+  toIsSpectralMap := hg.toIsSpectralMap.comp hf.toIsSpectralMap
+  image_closedPoints := by
+    intro x hx
+    exact hg.image_closedPoints (hf.image_closedPoints hx)
 
 lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X → Y}
     (hf : IsEmbedding f) (h : StableUnderSpecialization (Set.range f))
-    [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X :=
-  sorry
+    [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X where
+  eq_of_specializes {x c c'} hc hc' hxc hxc' := by
+    have closed_map_points (z : X) (hz : IsClosed ({z} : Set X)) :
+        IsClosed ({f z} : Set Y) := by
+      rw [← closure_eq_iff_isClosed]
+      apply Set.Subset.antisymm _ subset_closure
+      intro y hy
+      have hspec : f z ⤳ y := specializes_iff_mem_closure.mpr hy
+      have hfy : y ∈ Set.range f := h hspec (Set.mem_range_self z)
+      obtain ⟨z', rfl⟩ := hfy
+      have hzz' : z ⤳ z' := hf.specializes_iff.mp hspec
+      have : z' ∈ ({z} : Set X) := hz.closure_eq ▸ hzz'.mem_closure
+      rw [Set.mem_singleton_iff.mp this]
+      exact Set.mem_singleton _
+    exact hf.injective (WLocalSpace.eq_of_specializes (closed_map_points c hc)
+      (closed_map_points c' hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
+  isClosed_closedPoints := by
+    have closed_map_points (z : X) (hz : IsClosed ({z} : Set X)) :
+        IsClosed ({f z} : Set Y) := by
+      rw [← closure_eq_iff_isClosed]
+      apply Set.Subset.antisymm _ subset_closure
+      intro y hy
+      have hspec : f z ⤳ y := specializes_iff_mem_closure.mpr hy
+      have hfy : y ∈ Set.range f := h hspec (Set.mem_range_self z)
+      obtain ⟨z', rfl⟩ := hfy
+      have hzz' : z ⤳ z' := hf.specializes_iff.mp hspec
+      have : z' ∈ ({z} : Set X) := hz.closure_eq ▸ hzz'.mem_closure
+      rw [Set.mem_singleton_iff.mp this]
+      exact Set.mem_singleton _
+    have : closedPoints X = f ⁻¹' closedPoints Y := by
+      ext x
+      simp only [Set.mem_preimage, mem_closedPoints_iff]
+      constructor
+      · exact closed_map_points x
+      · intro hfx
+        rw [← closure_eq_iff_isClosed]
+        apply Set.Subset.antisymm _ subset_closure
+        intro x' hx'
+        have hspec : x ⤳ x' := specializes_iff_mem_closure.mpr hx'
+        have hfspec : f x ⤳ f x' := hspec.map hf.continuous
+        have hmem : f x' ∈ ({f x} : Set Y) := hfx.closure_eq ▸ hfspec.mem_closure
+        exact Set.mem_singleton_iff.mpr (hf.injective (Set.mem_singleton_iff.mp hmem))
+    rw [this]
+    exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
 
 lemma StableUnderSpecialization.generalizationHull_of_wLocalSpace [WLocalSpace X] {s : Set X}
     (hs : StableUnderSpecialization s) :
     StableUnderSpecialization (generalizationHull s) := by
-  sorry
+  rw [generalizationHull_eq]
+  intro a b hab ha
+  obtain ⟨y, hys, hay⟩ := ha
+  obtain ⟨c, hc_closed, hyc⟩ := exists_isClosed_specializes y
+  have hcs : c ∈ s := hs hyc hys
+  have hac : a ⤳ c := hay.trans hyc
+  obtain ⟨c', hc'_closed, hbc'⟩ := exists_isClosed_specializes b
+  have hac' : a ⤳ c' := hab.trans hbc'
+  have : c = c' := WLocalSpace.eq_of_specializes hc_closed hc'_closed hac hac'
+  subst this
+  exact ⟨c, hcs, hbc'⟩
 
 lemma Topology.IsClosedEmbedding.wLocalSpace {f : X → Y} (hf : IsClosedEmbedding f)
-    [WLocalSpace Y] : WLocalSpace X :=
-  sorry
+    [WLocalSpace Y] : WLocalSpace X where
+  toSpectralSpace := hf.spectralSpace
+  eq_of_specializes {x c c'} hc hc' hxc hxc' := by
+    have hfc : IsClosed ({f c} : Set Y) := by
+      rw [← Set.image_singleton]; exact hf.isClosedMap _ hc
+    have hfc' : IsClosed ({f c'} : Set Y) := by
+      rw [← Set.image_singleton]; exact hf.isClosedMap _ hc'
+    exact hf.injective (WLocalSpace.eq_of_specializes hfc hfc'
+      (hxc.map hf.continuous) (hxc'.map hf.continuous))
+  isClosed_closedPoints := by
+    have : closedPoints X = f ⁻¹' closedPoints Y := by
+      ext x
+      simp only [Set.mem_preimage, mem_closedPoints_iff]
+      constructor
+      · intro hx
+        rw [← Set.image_singleton]
+        exact hf.isClosedMap _ hx
+      · intro hfx
+        rwa [hf.isClosed_iff_image_isClosed, Set.image_singleton]
+    rw [this]
+    exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
 
 lemma isClosed_generalizationHull_of_wLocalSpace [WLocalSpace X] {s : Set X} (hs : IsClosed s) :
     IsClosed (generalizationHull s) :=

From 6b7b8ccabebc18bb41b92160f76b5bbc8c44ed55 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 12 Mar 2026 15:38:24 +0000
Subject: [PATCH 2/9] address review comments

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../Topology/SpectralSpace/WLocal/Basic.lean  | 72 +++++++++----------
 1 file changed, 33 insertions(+), 39 deletions(-)

diff --git a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
index 57d8723..c93badd 100644
--- a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
+++ b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
@@ -34,62 +34,57 @@ attribute [instance] WLocalSpace.isClosed_closedPoints
 @[mk_iff]
 structure IsWLocalMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop
     extends IsSpectralMap f where
-  image_closedPoints : closedPoints X ⊆ f ⁻¹' (closedPoints Y)
+  closedPoints_subset_preimage_closedPoints : closedPoints X ⊆ f ⁻¹' (closedPoints Y)
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
+/-- A w-local map sends closed points to closed points. -/
+lemma IsWLocalMap.isClosed_singleton {f : X → Y} (hf : IsWLocalMap f)
+    {x : X} (hx : IsClosed ({x} : Set X)) :
+    IsClosed ({f x} : Set Y) :=
+  mem_closedPoints_iff.mp
+    (hf.closedPoints_subset_preimage_closedPoints (mem_closedPoints_iff.mpr hx))
+
 lemma IsWLocalMap.comp {Z : Type*} [TopologicalSpace Z] {f : X → Y} {g : Y → Z}
     (hf : IsWLocalMap f) (hg : IsWLocalMap g) :
     IsWLocalMap (g ∘ f) where
   toIsSpectralMap := hg.toIsSpectralMap.comp hf.toIsSpectralMap
-  image_closedPoints := by
-    intro x hx
-    exact hg.image_closedPoints (hf.image_closedPoints hx)
+  closedPoints_subset_preimage_closedPoints _ hx :=
+    hg.closedPoints_subset_preimage_closedPoints
+      (hf.closedPoints_subset_preimage_closedPoints hx)
+
+/-- An embedding with specialization-stable range into a w-local space maps closed singletons
+to closed singletons. -/
+lemma Topology.IsEmbedding.isClosed_singleton_image
+    {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f))
+    [WLocalSpace Y] {z : X} (hz : IsClosed ({z} : Set X)) :
+    IsClosed ({f z} : Set Y) := by
+  rw [← closure_eq_iff_isClosed]
+  refine Set.Subset.antisymm (fun y hy => ?_) subset_closure
+  have hspec : f z ⤳ y := specializes_iff_mem_closure.mpr hy
+  obtain ⟨z', rfl⟩ := hrange hspec (Set.mem_range_self z)
+  have hzz' : z ⤳ z' := hf.specializes_iff.mp hspec
+  have : z' ∈ ({z} : Set X) := hz.closure_eq ▸ hzz'.mem_closure
+  rw [Set.mem_singleton_iff.mp this]
+  exact Set.mem_singleton _
 
 lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X → Y}
     (hf : IsEmbedding f) (h : StableUnderSpecialization (Set.range f))
     [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X where
-  eq_of_specializes {x c c'} hc hc' hxc hxc' := by
-    have closed_map_points (z : X) (hz : IsClosed ({z} : Set X)) :
-        IsClosed ({f z} : Set Y) := by
-      rw [← closure_eq_iff_isClosed]
-      apply Set.Subset.antisymm _ subset_closure
-      intro y hy
-      have hspec : f z ⤳ y := specializes_iff_mem_closure.mpr hy
-      have hfy : y ∈ Set.range f := h hspec (Set.mem_range_self z)
-      obtain ⟨z', rfl⟩ := hfy
-      have hzz' : z ⤳ z' := hf.specializes_iff.mp hspec
-      have : z' ∈ ({z} : Set X) := hz.closure_eq ▸ hzz'.mem_closure
-      rw [Set.mem_singleton_iff.mp this]
-      exact Set.mem_singleton _
-    exact hf.injective (WLocalSpace.eq_of_specializes (closed_map_points c hc)
-      (closed_map_points c' hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
+  eq_of_specializes {x c c'} hc hc' hxc hxc' :=
+    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosed_singleton_image h hc)
+      (hf.isClosed_singleton_image h hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
   isClosed_closedPoints := by
-    have closed_map_points (z : X) (hz : IsClosed ({z} : Set X)) :
-        IsClosed ({f z} : Set Y) := by
-      rw [← closure_eq_iff_isClosed]
-      apply Set.Subset.antisymm _ subset_closure
-      intro y hy
-      have hspec : f z ⤳ y := specializes_iff_mem_closure.mpr hy
-      have hfy : y ∈ Set.range f := h hspec (Set.mem_range_self z)
-      obtain ⟨z', rfl⟩ := hfy
-      have hzz' : z ⤳ z' := hf.specializes_iff.mp hspec
-      have : z' ∈ ({z} : Set X) := hz.closure_eq ▸ hzz'.mem_closure
-      rw [Set.mem_singleton_iff.mp this]
-      exact Set.mem_singleton _
     have : closedPoints X = f ⁻¹' closedPoints Y := by
       ext x
       simp only [Set.mem_preimage, mem_closedPoints_iff]
-      constructor
-      · exact closed_map_points x
-      · intro hfx
+      exact ⟨hf.isClosed_singleton_image h, fun hfx => by
         rw [← closure_eq_iff_isClosed]
-        apply Set.Subset.antisymm _ subset_closure
-        intro x' hx'
+        refine Set.Subset.antisymm (fun x' hx' => ?_) subset_closure
         have hspec : x ⤳ x' := specializes_iff_mem_closure.mpr hx'
         have hfspec : f x ⤳ f x' := hspec.map hf.continuous
         have hmem : f x' ∈ ({f x} : Set Y) := hfx.closure_eq ▸ hfspec.mem_closure
-        exact Set.mem_singleton_iff.mpr (hf.injective (Set.mem_singleton_iff.mp hmem))
+        exact Set.mem_singleton_iff.mpr (hf.injective (Set.mem_singleton_iff.mp hmem))⟩
     rw [this]
     exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
 
@@ -104,8 +99,7 @@ lemma StableUnderSpecialization.generalizationHull_of_wLocalSpace [WLocalSpace X
   have hac : a ⤳ c := hay.trans hyc
   obtain ⟨c', hc'_closed, hbc'⟩ := exists_isClosed_specializes b
   have hac' : a ⤳ c' := hab.trans hbc'
-  have : c = c' := WLocalSpace.eq_of_specializes hc_closed hc'_closed hac hac'
-  subst this
+  obtain rfl := WLocalSpace.eq_of_specializes hc_closed hc'_closed hac hac'
   exact ⟨c, hcs, hbc'⟩
 
 lemma Topology.IsClosedEmbedding.wLocalSpace {f : X → Y} (hf : IsClosedEmbedding f)

From 19097b7d59207fd60fbbe736322e01f4260e3b00 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 12 Mar 2026 19:17:32 +0000
Subject: [PATCH 3/9] address review comments (round 2)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../Topology/SpectralSpace/WLocal/Basic.lean  | 74 ++++++++++---------
 1 file changed, 41 insertions(+), 33 deletions(-)

diff --git a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
index c93badd..3744038 100644
--- a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
+++ b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
@@ -38,6 +38,19 @@ structure IsWLocalMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
+/-- A closed map sends closed singletons to closed singletons. -/
+lemma IsClosedMap.isClosed_singleton {f : X → Y} (hf : IsClosedMap f)
+    {x : X} (hx : IsClosed ({x} : Set X)) :
+    IsClosed ({f x} : Set Y) := by
+  rw [← Set.image_singleton]; exact hf _ hx
+
+/-- If `IsClosed ({x} : Set X) ↔ IsClosed ({f x} : Set Y)` for all `x`, then the closed
+points of `X` are exactly the preimage of the closed points of `Y`. -/
+lemma closedPoints_eq_preimage {f : X → Y}
+    (h : ∀ x : X, IsClosed ({x} : Set X) ↔ IsClosed ({f x} : Set Y)) :
+    closedPoints X = f ⁻¹' closedPoints Y :=
+  Set.ext fun x => by simp only [Set.mem_preimage, mem_closedPoints_iff, h]
+
 /-- A w-local map sends closed points to closed points. -/
 lemma IsWLocalMap.isClosed_singleton {f : X → Y} (hf : IsWLocalMap f)
     {x : X} (hx : IsClosed ({x} : Set X)) :
@@ -68,6 +81,24 @@ lemma Topology.IsEmbedding.isClosed_singleton_image
   rw [Set.mem_singleton_iff.mp this]
   exact Set.mem_singleton _
 
+/-- If `f` is an embedding and `{f z}` is closed, then `{z}` is closed. -/
+lemma Topology.IsEmbedding.isClosed_singleton_of_isClosed_image
+    {f : X → Y} (hf : IsEmbedding f) {z : X} (hz : IsClosed ({f z} : Set Y)) :
+    IsClosed ({z} : Set X) := by
+  rw [← closure_eq_iff_isClosed]
+  refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
+  have hfspec : f z ⤳ f x := (specializes_iff_mem_closure.mpr hx).map hf.continuous
+  exact Set.mem_singleton_iff.mpr
+    (hf.injective (Set.mem_singleton_iff.mp (hz.closure_eq ▸ hfspec.mem_closure)))
+
+/-- An embedding with specialization-stable range into a w-local space identifies
+closed points of `X` with the preimage of closed points of `Y`. -/
+lemma Topology.IsEmbedding.closedPoints_eq_preimage
+    {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f))
+    [WLocalSpace Y] : closedPoints X = f ⁻¹' closedPoints Y :=
+  _root_.closedPoints_eq_preimage fun _ =>
+    ⟨hf.isClosed_singleton_image hrange, hf.isClosed_singleton_of_isClosed_image⟩
+
 lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X → Y}
     (hf : IsEmbedding f) (h : StableUnderSpecialization (Set.range f))
     [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X where
@@ -75,17 +106,7 @@ lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X
     hf.injective (WLocalSpace.eq_of_specializes (hf.isClosed_singleton_image h hc)
       (hf.isClosed_singleton_image h hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
   isClosed_closedPoints := by
-    have : closedPoints X = f ⁻¹' closedPoints Y := by
-      ext x
-      simp only [Set.mem_preimage, mem_closedPoints_iff]
-      exact ⟨hf.isClosed_singleton_image h, fun hfx => by
-        rw [← closure_eq_iff_isClosed]
-        refine Set.Subset.antisymm (fun x' hx' => ?_) subset_closure
-        have hspec : x ⤳ x' := specializes_iff_mem_closure.mpr hx'
-        have hfspec : f x ⤳ f x' := hspec.map hf.continuous
-        have hmem : f x' ∈ ({f x} : Set Y) := hfx.closure_eq ▸ hfspec.mem_closure
-        exact Set.mem_singleton_iff.mpr (hf.injective (Set.mem_singleton_iff.mp hmem))⟩
-    rw [this]
+    rw [hf.closedPoints_eq_preimage h]
     exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
 
 lemma StableUnderSpecialization.generalizationHull_of_wLocalSpace [WLocalSpace X] {s : Set X}
@@ -95,34 +116,21 @@ lemma StableUnderSpecialization.generalizationHull_of_wLocalSpace [WLocalSpace X
   intro a b hab ha
   obtain ⟨y, hys, hay⟩ := ha
   obtain ⟨c, hc_closed, hyc⟩ := exists_isClosed_specializes y
-  have hcs : c ∈ s := hs hyc hys
-  have hac : a ⤳ c := hay.trans hyc
   obtain ⟨c', hc'_closed, hbc'⟩ := exists_isClosed_specializes b
-  have hac' : a ⤳ c' := hab.trans hbc'
-  obtain rfl := WLocalSpace.eq_of_specializes hc_closed hc'_closed hac hac'
-  exact ⟨c, hcs, hbc'⟩
+  obtain rfl := WLocalSpace.eq_of_specializes hc_closed hc'_closed
+    (hay.trans hyc) (hab.trans hbc')
+  exact ⟨c, hs hyc hys, hbc'⟩
 
 lemma Topology.IsClosedEmbedding.wLocalSpace {f : X → Y} (hf : IsClosedEmbedding f)
     [WLocalSpace Y] : WLocalSpace X where
   toSpectralSpace := hf.spectralSpace
-  eq_of_specializes {x c c'} hc hc' hxc hxc' := by
-    have hfc : IsClosed ({f c} : Set Y) := by
-      rw [← Set.image_singleton]; exact hf.isClosedMap _ hc
-    have hfc' : IsClosed ({f c'} : Set Y) := by
-      rw [← Set.image_singleton]; exact hf.isClosedMap _ hc'
-    exact hf.injective (WLocalSpace.eq_of_specializes hfc hfc'
-      (hxc.map hf.continuous) (hxc'.map hf.continuous))
+  eq_of_specializes {x c c'} hc hc' hxc hxc' :=
+    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosedMap.isClosed_singleton hc)
+      (hf.isClosedMap.isClosed_singleton hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
   isClosed_closedPoints := by
-    have : closedPoints X = f ⁻¹' closedPoints Y := by
-      ext x
-      simp only [Set.mem_preimage, mem_closedPoints_iff]
-      constructor
-      · intro hx
-        rw [← Set.image_singleton]
-        exact hf.isClosedMap _ hx
-      · intro hfx
-        rwa [hf.isClosed_iff_image_isClosed, Set.image_singleton]
-    rw [this]
+    rw [_root_.closedPoints_eq_preimage (f := f) fun x =>
+      ⟨hf.isClosedMap.isClosed_singleton, fun hfx => by
+        rwa [hf.isClosed_iff_image_isClosed, Set.image_singleton]⟩]
     exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
 
 lemma isClosed_generalizationHull_of_wLocalSpace [WLocalSpace X] {s : Set X} (hs : IsClosed s) :

From 40118502a75f4fc5a66ebff9745d4f2d3f3d99db Mon Sep 17 00:00:00 2001
From: Slopetale Agent <agent@slopetale.bot>
Date: Sat, 14 Mar 2026 17:38:32 +0000
Subject: [PATCH 4/9] address review comments on pr/wlocal-basic-proofs

- Remove trivial `closedPoints_eq_preimage` lemma
- Remove spurious `[WLocalSpace Y]` from `IsEmbedding.isClosed_singleton_image` and `IsEmbedding.closedPoints_eq_preimage`
- Simplify `IsClosedEmbedding.wLocalSpace` using `wLocalSpace_of_stableUnderSpecialization_range` and `IsClosed.stableUnderSpecialization`

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 .../Topology/SpectralSpace/WLocal/Basic.lean  | 37 ++++++-------------
 1 file changed, 12 insertions(+), 25 deletions(-)

diff --git a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
index 3744038..9b4bd36 100644
--- a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
+++ b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
@@ -44,13 +44,6 @@ lemma IsClosedMap.isClosed_singleton {f : X → Y} (hf : IsClosedMap f)
     IsClosed ({f x} : Set Y) := by
   rw [← Set.image_singleton]; exact hf _ hx
 
-/-- If `IsClosed ({x} : Set X) ↔ IsClosed ({f x} : Set Y)` for all `x`, then the closed
-points of `X` are exactly the preimage of the closed points of `Y`. -/
-lemma closedPoints_eq_preimage {f : X → Y}
-    (h : ∀ x : X, IsClosed ({x} : Set X) ↔ IsClosed ({f x} : Set Y)) :
-    closedPoints X = f ⁻¹' closedPoints Y :=
-  Set.ext fun x => by simp only [Set.mem_preimage, mem_closedPoints_iff, h]
-
 /-- A w-local map sends closed points to closed points. -/
 lemma IsWLocalMap.isClosed_singleton {f : X → Y} (hf : IsWLocalMap f)
     {x : X} (hx : IsClosed ({x} : Set X)) :
@@ -66,11 +59,10 @@ lemma IsWLocalMap.comp {Z : Type*} [TopologicalSpace Z] {f : X → Y} {g : Y →
     hg.closedPoints_subset_preimage_closedPoints
       (hf.closedPoints_subset_preimage_closedPoints hx)
 
-/-- An embedding with specialization-stable range into a w-local space maps closed singletons
-to closed singletons. -/
+/-- An embedding with specialization-stable range maps closed singletons to closed singletons. -/
 lemma Topology.IsEmbedding.isClosed_singleton_image
     {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f))
-    [WLocalSpace Y] {z : X} (hz : IsClosed ({z} : Set X)) :
+    {z : X} (hz : IsClosed ({z} : Set X)) :
     IsClosed ({f z} : Set Y) := by
   rw [← closure_eq_iff_isClosed]
   refine Set.Subset.antisymm (fun y hy => ?_) subset_closure
@@ -91,13 +83,14 @@ lemma Topology.IsEmbedding.isClosed_singleton_of_isClosed_image
   exact Set.mem_singleton_iff.mpr
     (hf.injective (Set.mem_singleton_iff.mp (hz.closure_eq ▸ hfspec.mem_closure)))
 
-/-- An embedding with specialization-stable range into a w-local space identifies
+/-- An embedding with specialization-stable range identifies
 closed points of `X` with the preimage of closed points of `Y`. -/
 lemma Topology.IsEmbedding.closedPoints_eq_preimage
-    {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f))
-    [WLocalSpace Y] : closedPoints X = f ⁻¹' closedPoints Y :=
-  _root_.closedPoints_eq_preimage fun _ =>
-    ⟨hf.isClosed_singleton_image hrange, hf.isClosed_singleton_of_isClosed_image⟩
+    {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f)) :
+    closedPoints X = f ⁻¹' closedPoints Y :=
+  Set.ext fun x => by
+    simp only [Set.mem_preimage, mem_closedPoints_iff]
+    exact ⟨hf.isClosed_singleton_image hrange, hf.isClosed_singleton_of_isClosed_image⟩
 
 lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X → Y}
     (hf : IsEmbedding f) (h : StableUnderSpecialization (Set.range f))
@@ -122,16 +115,10 @@ lemma StableUnderSpecialization.generalizationHull_of_wLocalSpace [WLocalSpace X
   exact ⟨c, hs hyc hys, hbc'⟩
 
 lemma Topology.IsClosedEmbedding.wLocalSpace {f : X → Y} (hf : IsClosedEmbedding f)
-    [WLocalSpace Y] : WLocalSpace X where
-  toSpectralSpace := hf.spectralSpace
-  eq_of_specializes {x c c'} hc hc' hxc hxc' :=
-    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosedMap.isClosed_singleton hc)
-      (hf.isClosedMap.isClosed_singleton hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
-  isClosed_closedPoints := by
-    rw [_root_.closedPoints_eq_preimage (f := f) fun x =>
-      ⟨hf.isClosedMap.isClosed_singleton, fun hfx => by
-        rwa [hf.isClosed_iff_image_isClosed, Set.image_singleton]⟩]
-    exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
+    [WLocalSpace Y] : WLocalSpace X :=
+  haveI : SpectralSpace X := hf.spectralSpace
+  hf.isEmbedding.wLocalSpace_of_stableUnderSpecialization_range
+    hf.isClosedMap.isClosed_range.stableUnderSpecialization
 
 lemma isClosed_generalizationHull_of_wLocalSpace [WLocalSpace X] {s : Set X} (hs : IsClosed s) :
     IsClosed (generalizationHull s) :=

From eae677bb63468708ba786e371b7b6950b5fee942 Mon Sep 17 00:00:00 2001
From: Slopetale Agent <agent@slopetale.bot>
Date: Mon, 16 Mar 2026 16:25:45 +0000
Subject: [PATCH 5/9] style(Topology/SpectralSpace/WLocal/Basic): fix style and
 naming issues
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Split semicolon-chained tactics onto separate lines
- Rename `isClosed_singleton` → `isClosed_image_singleton` in
  `IsClosedMap` and `IsWLocalMap` namespaces to clarify the name
  describes the image of a singleton
- Rename `IsEmbedding.isClosed_singleton_image` →
  `IsEmbedding.isClosed_image_singleton` for consistency with Mathlib
  naming convention
- Rename `IsEmbedding.isClosed_singleton_of_isClosed_image` →
  `IsEmbedding.isClosed_singleton_of_isClosed_image_singleton` to
  make clear the hypothesis concerns an image singleton

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 .../Topology/SpectralSpace/WLocal/Basic.lean    | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
index 9b4bd36..498cb56 100644
--- a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
+++ b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
@@ -39,13 +39,14 @@ structure IsWLocalMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
 /-- A closed map sends closed singletons to closed singletons. -/
-lemma IsClosedMap.isClosed_singleton {f : X → Y} (hf : IsClosedMap f)
+lemma IsClosedMap.isClosed_image_singleton {f : X → Y} (hf : IsClosedMap f)
     {x : X} (hx : IsClosed ({x} : Set X)) :
     IsClosed ({f x} : Set Y) := by
-  rw [← Set.image_singleton]; exact hf _ hx
+  rw [← Set.image_singleton]
+  exact hf _ hx
 
 /-- A w-local map sends closed points to closed points. -/
-lemma IsWLocalMap.isClosed_singleton {f : X → Y} (hf : IsWLocalMap f)
+lemma IsWLocalMap.isClosed_image_singleton {f : X → Y} (hf : IsWLocalMap f)
     {x : X} (hx : IsClosed ({x} : Set X)) :
     IsClosed ({f x} : Set Y) :=
   mem_closedPoints_iff.mp
@@ -60,7 +61,7 @@ lemma IsWLocalMap.comp {Z : Type*} [TopologicalSpace Z] {f : X → Y} {g : Y →
       (hf.closedPoints_subset_preimage_closedPoints hx)
 
 /-- An embedding with specialization-stable range maps closed singletons to closed singletons. -/
-lemma Topology.IsEmbedding.isClosed_singleton_image
+lemma Topology.IsEmbedding.isClosed_image_singleton
     {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f))
     {z : X} (hz : IsClosed ({z} : Set X)) :
     IsClosed ({f z} : Set Y) := by
@@ -74,7 +75,7 @@ lemma Topology.IsEmbedding.isClosed_singleton_image
   exact Set.mem_singleton _
 
 /-- If `f` is an embedding and `{f z}` is closed, then `{z}` is closed. -/
-lemma Topology.IsEmbedding.isClosed_singleton_of_isClosed_image
+lemma Topology.IsEmbedding.isClosed_singleton_of_isClosed_image_singleton
     {f : X → Y} (hf : IsEmbedding f) {z : X} (hz : IsClosed ({f z} : Set Y)) :
     IsClosed ({z} : Set X) := by
   rw [← closure_eq_iff_isClosed]
@@ -90,14 +91,14 @@ lemma Topology.IsEmbedding.closedPoints_eq_preimage
     closedPoints X = f ⁻¹' closedPoints Y :=
   Set.ext fun x => by
     simp only [Set.mem_preimage, mem_closedPoints_iff]
-    exact ⟨hf.isClosed_singleton_image hrange, hf.isClosed_singleton_of_isClosed_image⟩
+    exact ⟨hf.isClosed_image_singleton hrange, hf.isClosed_singleton_of_isClosed_image_singleton⟩
 
 lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X → Y}
     (hf : IsEmbedding f) (h : StableUnderSpecialization (Set.range f))
     [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X where
   eq_of_specializes {x c c'} hc hc' hxc hxc' :=
-    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosed_singleton_image h hc)
-      (hf.isClosed_singleton_image h hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
+    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosed_image_singleton h hc)
+      (hf.isClosed_image_singleton h hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
   isClosed_closedPoints := by
     rw [hf.closedPoints_eq_preimage h]
     exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous

From 0a2218e84ee7a354390ee8d71f5643a385ff072d Mon Sep 17 00:00:00 2001
From: Slopetale Agent <agent@slopetale.bot>
Date: Mon, 16 Mar 2026 16:49:47 +0000
Subject: [PATCH 6/9] address review comments

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 .../Mathlib/Topology/Separation/Basic.lean    |  9 +++++
 .../Topology/SpectralSpace/WLocal/Basic.lean  | 37 ++++++++-----------
 2 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/Proetale/Mathlib/Topology/Separation/Basic.lean b/Proetale/Mathlib/Topology/Separation/Basic.lean
index 310a654..2e94587 100644
--- a/Proetale/Mathlib/Topology/Separation/Basic.lean
+++ b/Proetale/Mathlib/Topology/Separation/Basic.lean
@@ -1,5 +1,14 @@
 import Mathlib.Topology.Separation.Basic
 
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+
+/-- A closed map sends closed singletons to closed singletons. -/
+lemma IsClosedMap.isClosed_singleton {f : X → Y} (hf : IsClosedMap f)
+    {x : X} (hx : IsClosed {x}) :
+    IsClosed {f x} := by
+  rw [← Set.image_singleton]
+  exact hf _ hx
+
 /-- In a compact, T0 space every point specializes to a (not necessarily unique) closed point. -/
 lemma exists_isClosed_specializes {X : Type*} [TopologicalSpace X] [CompactSpace X]
     [T0Space X] (x : X) :
diff --git a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
index 498cb56..216cf70 100644
--- a/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
+++ b/Proetale/Topology/SpectralSpace/WLocal/Basic.lean
@@ -38,17 +38,10 @@ structure IsWLocalMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
-/-- A closed map sends closed singletons to closed singletons. -/
-lemma IsClosedMap.isClosed_image_singleton {f : X → Y} (hf : IsClosedMap f)
-    {x : X} (hx : IsClosed ({x} : Set X)) :
-    IsClosed ({f x} : Set Y) := by
-  rw [← Set.image_singleton]
-  exact hf _ hx
-
 /-- A w-local map sends closed points to closed points. -/
-lemma IsWLocalMap.isClosed_image_singleton {f : X → Y} (hf : IsWLocalMap f)
-    {x : X} (hx : IsClosed ({x} : Set X)) :
-    IsClosed ({f x} : Set Y) :=
+lemma IsWLocalMap.isClosed_singleton {f : X → Y} (hf : IsWLocalMap f)
+    {x : X} (hx : IsClosed {x}) :
+    IsClosed {f x} :=
   mem_closedPoints_iff.mp
     (hf.closedPoints_subset_preimage_closedPoints (mem_closedPoints_iff.mpr hx))
 
@@ -61,10 +54,10 @@ lemma IsWLocalMap.comp {Z : Type*} [TopologicalSpace Z] {f : X → Y} {g : Y →
       (hf.closedPoints_subset_preimage_closedPoints hx)
 
 /-- An embedding with specialization-stable range maps closed singletons to closed singletons. -/
-lemma Topology.IsEmbedding.isClosed_image_singleton
+lemma Topology.IsEmbedding.isClosed_singleton
     {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f))
-    {z : X} (hz : IsClosed ({z} : Set X)) :
-    IsClosed ({f z} : Set Y) := by
+    {z : X} (hz : IsClosed {z}) :
+    IsClosed {f z} := by
   rw [← closure_eq_iff_isClosed]
   refine Set.Subset.antisymm (fun y hy => ?_) subset_closure
   have hspec : f z ⤳ y := specializes_iff_mem_closure.mpr hy
@@ -76,8 +69,8 @@ lemma Topology.IsEmbedding.isClosed_image_singleton
 
 /-- If `f` is an embedding and `{f z}` is closed, then `{z}` is closed. -/
 lemma Topology.IsEmbedding.isClosed_singleton_of_isClosed_image_singleton
-    {f : X → Y} (hf : IsEmbedding f) {z : X} (hz : IsClosed ({f z} : Set Y)) :
-    IsClosed ({z} : Set X) := by
+    {f : X → Y} (hf : IsEmbedding f) {z : X} (hz : IsClosed {f z}) :
+    IsClosed {z} := by
   rw [← closure_eq_iff_isClosed]
   refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
   have hfspec : f z ⤳ f x := (specializes_iff_mem_closure.mpr hx).map hf.continuous
@@ -88,17 +81,17 @@ lemma Topology.IsEmbedding.isClosed_singleton_of_isClosed_image_singleton
 closed points of `X` with the preimage of closed points of `Y`. -/
 lemma Topology.IsEmbedding.closedPoints_eq_preimage
     {f : X → Y} (hf : IsEmbedding f) (hrange : StableUnderSpecialization (Set.range f)) :
-    closedPoints X = f ⁻¹' closedPoints Y :=
-  Set.ext fun x => by
-    simp only [Set.mem_preimage, mem_closedPoints_iff]
-    exact ⟨hf.isClosed_image_singleton hrange, hf.isClosed_singleton_of_isClosed_image_singleton⟩
+    closedPoints X = f ⁻¹' closedPoints Y := by
+  ext x
+  simp only [Set.mem_preimage, mem_closedPoints_iff]
+  exact ⟨hf.isClosed_singleton hrange, hf.isClosed_singleton_of_isClosed_image_singleton⟩
 
 lemma Topology.IsEmbedding.wLocalSpace_of_stableUnderSpecialization_range {f : X → Y}
     (hf : IsEmbedding f) (h : StableUnderSpecialization (Set.range f))
     [SpectralSpace X] [WLocalSpace Y] : WLocalSpace X where
   eq_of_specializes {x c c'} hc hc' hxc hxc' :=
-    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosed_image_singleton h hc)
-      (hf.isClosed_image_singleton h hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
+    hf.injective (WLocalSpace.eq_of_specializes (hf.isClosed_singleton h hc)
+      (hf.isClosed_singleton h hc') (hxc.map hf.continuous) (hxc'.map hf.continuous))
   isClosed_closedPoints := by
     rw [hf.closedPoints_eq_preimage h]
     exact WLocalSpace.isClosed_closedPoints.preimage hf.continuous
@@ -117,7 +110,7 @@ lemma StableUnderSpecialization.generalizationHull_of_wLocalSpace [WLocalSpace X
 
 lemma Topology.IsClosedEmbedding.wLocalSpace {f : X → Y} (hf : IsClosedEmbedding f)
     [WLocalSpace Y] : WLocalSpace X :=
-  haveI : SpectralSpace X := hf.spectralSpace
+  have : SpectralSpace X := hf.spectralSpace
   hf.isEmbedding.wLocalSpace_of_stableUnderSpecialization_range
     hf.isClosedMap.isClosed_range.stableUnderSpecialization
 

From 437b957bfd68cf7c8c3b36de02c4823dacc5c3ba Mon Sep 17 00:00:00 2001
From: Slopetale Agent <agent@slopetale.bot>
Date: Mon, 16 Mar 2026 17:07:15 +0000
Subject: [PATCH 7/9] address review comments
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Revert unrelated change at line 97 (`by simp [isClopen_univ]` → `isClopen_univ, Set.mem_univ x`)
- Fix `rw [(t2Space_iff _)]` → `rw [t2Space_iff]`
- Extract `hsat` block as `IsClopen.connectedComponents_image_isClopen` in `TotallyDisconnected.lean` (earlier in hierarchy)
- Restore proofs for `t2Space_connectedComponent` and `lift_bijective_of_isPullback`

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 .../Connected/TotallyDisconnected.lean        |   8 ++
 .../SpectralSpace/ConnectedComponent.lean     | 128 +++++++++++++++++-
 2 files changed, 131 insertions(+), 5 deletions(-)

diff --git a/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean
index 8d0ecef..178e8e6 100644
--- a/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean
+++ b/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean
@@ -56,6 +56,14 @@ theorem Continuous.connectedComponentsLift_injective {X : Type*} [TopologicalSpa
   have hba : b = a := by simpa [Set.mem_singleton_iff] using this
   exact hba.symm
 
+theorem IsClopen.connectedComponents_image_isClopen {U : Set X} (hU : IsClopen U) :
+    IsClopen (ConnectedComponents.mk '' U : Set (ConnectedComponents X)) := by
+  have hsat : ConnectedComponents.mk ⁻¹'
+      (ConnectedComponents.mk '' U : Set (ConnectedComponents X)) = U := by
+    rw [connectedComponents_preimage_image]
+    exact hU.biUnion_connectedComponent_eq
+  rwa [← ConnectedComponents.isQuotientMap_coe.isClopen_preimage, hsat]
+
 -- end of the file
 variable (S T : Type*) [TopologicalSpace S] [TopologicalSpace T]
 
diff --git a/Proetale/Topology/SpectralSpace/ConnectedComponent.lean b/Proetale/Topology/SpectralSpace/ConnectedComponent.lean
index 108d9df..427982f 100644
--- a/Proetale/Topology/SpectralSpace/ConnectedComponent.lean
+++ b/Proetale/Topology/SpectralSpace/ConnectedComponent.lean
@@ -94,7 +94,7 @@ theorem sInter_isClopen_and_mem_eq_connectedComponent {x : X} :
     · rw [U.inter_comm, V.inter_comm, hUSB, hVSC]
       exact ⟨hBn, hCn⟩
   obtain ⟨U, V, hU, hV, hUc, hVc, hUVS, hSUV, hUSn, hVSn⟩ := this
-  have : Nonempty {U // IsClopen U ∧ x ∈ U} := ⟨⟨⊤, by simp [isClopen_univ]⟩⟩
+  have : Nonempty {U // IsClopen U ∧ x ∈ U} := ⟨⟨⊤, isClopen_univ, Set.mem_univ x⟩⟩
   obtain ⟨W, hxW, hW, hUVW⟩ : ∃ W : Set X, x ∈ W ∧ IsClopen W ∧ U ∩ V ∩ W = ∅ := by
     obtain ⟨W, hW⟩ := IsCompact.elim_directed_family_closed
       (IsCompact.inter_of_isOpen hUc hVc hU hV) _ (·.2.1.1) hUVS
@@ -255,9 +255,33 @@ instance compactSpace_connectedComponent {X : Type u} [TopologicalSpace X] [Comp
 
 @[stacks 0906]
 instance t2Space_connectedComponent {X : Type u} [TopologicalSpace X]  [CompactSpace X]
-    [QuasiSeparatedSpace X] [PrespectralSpace X] : T2Space (ConnectedComponents X) :=
-  sorry
-  -- use `isClosed_and_iUnion_connectedComponent_eq_iff`
+    [QuasiSeparatedSpace X] [PrespectralSpace X] : T2Space (ConnectedComponents X) := by
+  rw [t2Space_iff]
+  intro a b hab
+  -- Pick representatives
+  obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe a
+  obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe b
+  rw [ConnectedComponents.coe_ne_coe] at hab
+  -- y ∉ connectedComponent x
+  have hy : y ∉ connectedComponent x := fun h => hab (connectedComponent_eq h)
+  -- connectedComponent x = ⋂ {U | IsClopen U ∧ x ∈ U}, so ∃ clopen U with x ∈ U and y ∉ U
+  have hy' : ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U := by
+    by_contra! habs
+    apply hy
+    rw [← sInter_isClopen_and_mem_eq_connectedComponent]
+    exact Set.mem_iInter.mpr fun ⟨U, hU1, hU2⟩ => habs U hU1 hU2
+  obtain ⟨U, hU, hxU, hyU⟩ := hy'
+  -- mk '' U is clopen in ConnectedComponents X
+  have hU' : IsClopen (ConnectedComponents.mk '' U : Set (ConnectedComponents X)) :=
+    IsClopen.connectedComponents_image_isClopen hU
+  -- Use clopen set to separate: mk '' U and (mk '' U)ᶜ are disjoint open neighborhoods
+  refine ⟨ConnectedComponents.mk '' U, (ConnectedComponents.mk '' U)ᶜ, hU'.2,
+    hU'.1.isOpen_compl, Set.mem_image_of_mem _ hxU, ?_, disjoint_compl_right⟩
+  simp only [Set.mem_compl_iff, Set.mem_image, not_exists, not_and]
+  intro z hzU hzy
+  apply hyU
+  rw [ConnectedComponents.coe_eq_coe'] at hzy
+  exact hU.connectedComponent_subset hzU (connectedComponent_eq_iff_mem.mp (connectedComponent_eq hzy))
 
 end
 
@@ -277,7 +301,101 @@ theorem ConnectedComponents.lift_bijective_of_isPullback {Y T : Type u} [Topolog
     [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T]
     {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)}
     (pb : IsPullback (ofHom g) (ofHom f) (ofHom i) (ofHom ⟨mk, continuous_coe⟩)) :
-    Function.Bijective (connectedComponentsLift g.2) := sorry
+    Function.Bijective (connectedComponentsLift g.2) := by
+  -- The commutativity: i ∘ g = mk ∘ f (from fst ≫ f = snd ≫ g, i.e., g ≫ i = f ≫ mk)
+  have hw : ∀ y : Y, i (g y) = (f y : ConnectedComponents X) :=
+    fun y => ConcreteCategory.congr_hom pb.w y
+  constructor
+  · -- Injectivity: use connectedComponentsLift_injective by showing fibers of g are preconnected.
+    -- The fiber g⁻¹'{t} is homeomorphic (via the pullback) to a connected component of X.
+    apply g.2.connectedComponentsLift_injective
+    intro t
+    -- Construct the homeomorphism E : Y ≃ₜ {p : T × X | i p.1 = mk p.2}
+    have inst_hp := pb.hasPullback
+    let E := homeoOfIso (pb.isoPullback ≪≫
+      pullbackIsoProdSubtype (ofHom i) (ofHom ⟨mk, continuous_coe⟩))
+    -- Key property: g = fst ∘ E
+    have hE_g : ∀ y, (E y).val.1 = g y := by
+      intro y
+      show ((pb.isoPullback ≪≫
+        pullbackIsoProdSubtype (ofHom i) (ofHom ⟨mk, continuous_coe⟩)).hom y).val.1 = _
+      simp only [Iso.trans_hom, ConcreteCategory.comp_apply]
+      rw [pullbackIsoProdSubtype_hom_apply]
+      exact ConcreteCategory.congr_hom pb.isoPullback_hom_fst y
+    -- Key property: f = snd ∘ E
+    have hE_f : ∀ y, (E y).val.2 = f y := by
+      intro y
+      show ((pb.isoPullback ≪≫
+        pullbackIsoProdSubtype (ofHom i) (ofHom ⟨mk, continuous_coe⟩)).hom y).val.2 = _
+      simp only [Iso.trans_hom, ConcreteCategory.comp_apply]
+      rw [pullbackIsoProdSubtype_hom_apply]
+      exact ConcreteCategory.congr_hom pb.isoPullback_hom_snd y
+    -- The fiber g⁻¹'{t} is preconnected because it is the continuous image
+    -- of a connected component of X under the inverse of the pullback homeomorphism.
+    -- First handle the empty case.
+    by_cases hne : (g ⁻¹' {t}).Nonempty
+    swap
+    · exact (Set.not_nonempty_iff_eq_empty.mp hne) ▸ isPreconnected_empty
+    obtain ⟨y₀, hy₀⟩ := hne
+    have hy₀t : g y₀ = t := Set.mem_singleton_iff.mp hy₀
+    -- Define φ : {x : X | mk x = i t} → Y by φ(x) = E⁻¹(⟨(t, x), proof⟩)
+    let φ : {x : X | (x : ConnectedComponents X) = i t} → Y :=
+      fun x => E.symm ⟨(t, x.val), x.prop.symm⟩
+    -- φ is continuous
+    have hφ_cont : Continuous φ := by
+      show Continuous (E.symm ∘ (fun x : {x : X | (x : ConnectedComponents X) = i t} =>
+        (⟨(t, x.val), x.prop.symm⟩ : { p : T × X | i p.1 = (p.2 : ConnectedComponents X)})))
+      apply E.symm.continuous.comp
+      exact Continuous.subtype_mk (by fun_prop) _
+    -- φ maps into g⁻¹'{t}
+    have hφ_img : ∀ x, g (φ x) = t := by
+      intro ⟨x, hx⟩
+      show g (E.symm ⟨(t, x), hx.symm⟩) = t
+      conv_lhs => rw [← hE_g (E.symm ⟨(t, x), hx.symm⟩), E.apply_symm_apply]
+    -- φ is surjective onto g⁻¹'{t}
+    have hφ_surj : ∀ y, y ∈ g ⁻¹' {t} → y ∈ Set.range φ := by
+      intro y hy
+      have hyt : g y = t := Set.mem_singleton_iff.mp hy
+      have hmk : (f y : ConnectedComponents X) = i t := by
+        rw [← hw y, hyt]
+      refine ⟨⟨f y, hmk⟩, ?_⟩
+      show E.symm ⟨(t, f y), hmk.symm⟩ = y
+      apply E.injective
+      simp only [Homeomorph.apply_symm_apply]
+      apply Subtype.ext
+      apply Prod.ext
+      · simp only [hE_g]; exact hyt.symm
+      · exact (hE_f y).symm
+    -- {x : X | mk x = i t} = connectedComponent (f y₀), which is preconnected.
+    have hit : i t = (f y₀ : ConnectedComponents X) := by rw [← hw y₀, hy₀t]
+    have hconn : IsPreconnected {x : X | (x : ConnectedComponents X) = i t} := by
+      suffices h : {x : X | (x : ConnectedComponents X) = i t} = connectedComponent (f y₀) by
+        rw [h]; exact isConnected_connectedComponent.isPreconnected
+      ext x
+      simp only [Set.mem_setOf_eq, hit]
+      exact ConnectedComponents.coe_eq_coe'
+    -- The fiber g⁻¹'{t} is the image of a preconnected set under φ, hence preconnected.
+    have heq : g ⁻¹' {t} = Set.range φ := by
+      ext y
+      simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_range]
+      exact ⟨fun hy => hφ_surj y hy, fun ⟨x, hx⟩ => hx ▸ hφ_img x⟩
+    -- The domain of φ has preconnected space.
+    have : PreconnectedSpace {x : X | (x : ConnectedComponents X) = i t} :=
+      Subtype.preconnectedSpace hconn
+    show IsPreconnected (g.toFun ⁻¹' {t})
+    rw [show g.toFun ⁻¹' {t} = Set.range φ from heq]
+    exact isPreconnected_range hφ_cont
+  · -- Surjectivity: for each t : T, find y : Y with g y = t, giving lift(mk y) = g y = t.
+    intro t
+    obtain ⟨x, hx⟩ := ConnectedComponents.surjective_coe (i t)
+    let y := pb.lift (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} t))
+      (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} x))
+      (by ext ⟨⟩; exact hx.symm) PUnit.unit
+    have hgy : g y = t := ConcreteCategory.congr_hom
+      (pb.lift_fst (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} t))
+        (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} x))
+        (by ext ⟨⟩; exact hx.symm)) PUnit.unit
+    exact ⟨mk y, g.2.connectedComponentsLift_apply_coe y ▸ hgy⟩
 
 @[stacks 096C "first part"]
 theorem ConnectedComponents.isHomeomorph_lift_of_isPullback {Y T : Type u} [TopologicalSpace Y]

From 8b8c52b49bac327a5fd9a5cc54c82d1bf6c22b83 Mon Sep 17 00:00:00 2001
From: Slopetale Agent <agent@slopetale.bot>
Date: Mon, 16 Mar 2026 17:18:05 +0000
Subject: [PATCH 8/9] Revert "address review comments"

This reverts commit 437b957bfd68cf7c8c3b36de02c4823dacc5c3ba.
---
 .../Connected/TotallyDisconnected.lean        |   8 --
 .../SpectralSpace/ConnectedComponent.lean     | 128 +-----------------
 2 files changed, 5 insertions(+), 131 deletions(-)

diff --git a/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean
index 178e8e6..8d0ecef 100644
--- a/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean
+++ b/Proetale/Mathlib/Topology/Connected/TotallyDisconnected.lean
@@ -56,14 +56,6 @@ theorem Continuous.connectedComponentsLift_injective {X : Type*} [TopologicalSpa
   have hba : b = a := by simpa [Set.mem_singleton_iff] using this
   exact hba.symm
 
-theorem IsClopen.connectedComponents_image_isClopen {U : Set X} (hU : IsClopen U) :
-    IsClopen (ConnectedComponents.mk '' U : Set (ConnectedComponents X)) := by
-  have hsat : ConnectedComponents.mk ⁻¹'
-      (ConnectedComponents.mk '' U : Set (ConnectedComponents X)) = U := by
-    rw [connectedComponents_preimage_image]
-    exact hU.biUnion_connectedComponent_eq
-  rwa [← ConnectedComponents.isQuotientMap_coe.isClopen_preimage, hsat]
-
 -- end of the file
 variable (S T : Type*) [TopologicalSpace S] [TopologicalSpace T]
 
diff --git a/Proetale/Topology/SpectralSpace/ConnectedComponent.lean b/Proetale/Topology/SpectralSpace/ConnectedComponent.lean
index 427982f..108d9df 100644
--- a/Proetale/Topology/SpectralSpace/ConnectedComponent.lean
+++ b/Proetale/Topology/SpectralSpace/ConnectedComponent.lean
@@ -94,7 +94,7 @@ theorem sInter_isClopen_and_mem_eq_connectedComponent {x : X} :
     · rw [U.inter_comm, V.inter_comm, hUSB, hVSC]
       exact ⟨hBn, hCn⟩
   obtain ⟨U, V, hU, hV, hUc, hVc, hUVS, hSUV, hUSn, hVSn⟩ := this
-  have : Nonempty {U // IsClopen U ∧ x ∈ U} := ⟨⟨⊤, isClopen_univ, Set.mem_univ x⟩⟩
+  have : Nonempty {U // IsClopen U ∧ x ∈ U} := ⟨⟨⊤, by simp [isClopen_univ]⟩⟩
   obtain ⟨W, hxW, hW, hUVW⟩ : ∃ W : Set X, x ∈ W ∧ IsClopen W ∧ U ∩ V ∩ W = ∅ := by
     obtain ⟨W, hW⟩ := IsCompact.elim_directed_family_closed
       (IsCompact.inter_of_isOpen hUc hVc hU hV) _ (·.2.1.1) hUVS
@@ -255,33 +255,9 @@ instance compactSpace_connectedComponent {X : Type u} [TopologicalSpace X] [Comp
 
 @[stacks 0906]
 instance t2Space_connectedComponent {X : Type u} [TopologicalSpace X]  [CompactSpace X]
-    [QuasiSeparatedSpace X] [PrespectralSpace X] : T2Space (ConnectedComponents X) := by
-  rw [t2Space_iff]
-  intro a b hab
-  -- Pick representatives
-  obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe a
-  obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe b
-  rw [ConnectedComponents.coe_ne_coe] at hab
-  -- y ∉ connectedComponent x
-  have hy : y ∉ connectedComponent x := fun h => hab (connectedComponent_eq h)
-  -- connectedComponent x = ⋂ {U | IsClopen U ∧ x ∈ U}, so ∃ clopen U with x ∈ U and y ∉ U
-  have hy' : ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U := by
-    by_contra! habs
-    apply hy
-    rw [← sInter_isClopen_and_mem_eq_connectedComponent]
-    exact Set.mem_iInter.mpr fun ⟨U, hU1, hU2⟩ => habs U hU1 hU2
-  obtain ⟨U, hU, hxU, hyU⟩ := hy'
-  -- mk '' U is clopen in ConnectedComponents X
-  have hU' : IsClopen (ConnectedComponents.mk '' U : Set (ConnectedComponents X)) :=
-    IsClopen.connectedComponents_image_isClopen hU
-  -- Use clopen set to separate: mk '' U and (mk '' U)ᶜ are disjoint open neighborhoods
-  refine ⟨ConnectedComponents.mk '' U, (ConnectedComponents.mk '' U)ᶜ, hU'.2,
-    hU'.1.isOpen_compl, Set.mem_image_of_mem _ hxU, ?_, disjoint_compl_right⟩
-  simp only [Set.mem_compl_iff, Set.mem_image, not_exists, not_and]
-  intro z hzU hzy
-  apply hyU
-  rw [ConnectedComponents.coe_eq_coe'] at hzy
-  exact hU.connectedComponent_subset hzU (connectedComponent_eq_iff_mem.mp (connectedComponent_eq hzy))
+    [QuasiSeparatedSpace X] [PrespectralSpace X] : T2Space (ConnectedComponents X) :=
+  sorry
+  -- use `isClosed_and_iUnion_connectedComponent_eq_iff`
 
 end
 
@@ -301,101 +277,7 @@ theorem ConnectedComponents.lift_bijective_of_isPullback {Y T : Type u} [Topolog
     [TopologicalSpace T] [CompactSpace T] [T2Space T] [TotallyDisconnectedSpace T]
     {f : C(Y, X)} {g : C(Y, T)} {i : C(T, ConnectedComponents X)}
     (pb : IsPullback (ofHom g) (ofHom f) (ofHom i) (ofHom ⟨mk, continuous_coe⟩)) :
-    Function.Bijective (connectedComponentsLift g.2) := by
-  -- The commutativity: i ∘ g = mk ∘ f (from fst ≫ f = snd ≫ g, i.e., g ≫ i = f ≫ mk)
-  have hw : ∀ y : Y, i (g y) = (f y : ConnectedComponents X) :=
-    fun y => ConcreteCategory.congr_hom pb.w y
-  constructor
-  · -- Injectivity: use connectedComponentsLift_injective by showing fibers of g are preconnected.
-    -- The fiber g⁻¹'{t} is homeomorphic (via the pullback) to a connected component of X.
-    apply g.2.connectedComponentsLift_injective
-    intro t
-    -- Construct the homeomorphism E : Y ≃ₜ {p : T × X | i p.1 = mk p.2}
-    have inst_hp := pb.hasPullback
-    let E := homeoOfIso (pb.isoPullback ≪≫
-      pullbackIsoProdSubtype (ofHom i) (ofHom ⟨mk, continuous_coe⟩))
-    -- Key property: g = fst ∘ E
-    have hE_g : ∀ y, (E y).val.1 = g y := by
-      intro y
-      show ((pb.isoPullback ≪≫
-        pullbackIsoProdSubtype (ofHom i) (ofHom ⟨mk, continuous_coe⟩)).hom y).val.1 = _
-      simp only [Iso.trans_hom, ConcreteCategory.comp_apply]
-      rw [pullbackIsoProdSubtype_hom_apply]
-      exact ConcreteCategory.congr_hom pb.isoPullback_hom_fst y
-    -- Key property: f = snd ∘ E
-    have hE_f : ∀ y, (E y).val.2 = f y := by
-      intro y
-      show ((pb.isoPullback ≪≫
-        pullbackIsoProdSubtype (ofHom i) (ofHom ⟨mk, continuous_coe⟩)).hom y).val.2 = _
-      simp only [Iso.trans_hom, ConcreteCategory.comp_apply]
-      rw [pullbackIsoProdSubtype_hom_apply]
-      exact ConcreteCategory.congr_hom pb.isoPullback_hom_snd y
-    -- The fiber g⁻¹'{t} is preconnected because it is the continuous image
-    -- of a connected component of X under the inverse of the pullback homeomorphism.
-    -- First handle the empty case.
-    by_cases hne : (g ⁻¹' {t}).Nonempty
-    swap
-    · exact (Set.not_nonempty_iff_eq_empty.mp hne) ▸ isPreconnected_empty
-    obtain ⟨y₀, hy₀⟩ := hne
-    have hy₀t : g y₀ = t := Set.mem_singleton_iff.mp hy₀
-    -- Define φ : {x : X | mk x = i t} → Y by φ(x) = E⁻¹(⟨(t, x), proof⟩)
-    let φ : {x : X | (x : ConnectedComponents X) = i t} → Y :=
-      fun x => E.symm ⟨(t, x.val), x.prop.symm⟩
-    -- φ is continuous
-    have hφ_cont : Continuous φ := by
-      show Continuous (E.symm ∘ (fun x : {x : X | (x : ConnectedComponents X) = i t} =>
-        (⟨(t, x.val), x.prop.symm⟩ : { p : T × X | i p.1 = (p.2 : ConnectedComponents X)})))
-      apply E.symm.continuous.comp
-      exact Continuous.subtype_mk (by fun_prop) _
-    -- φ maps into g⁻¹'{t}
-    have hφ_img : ∀ x, g (φ x) = t := by
-      intro ⟨x, hx⟩
-      show g (E.symm ⟨(t, x), hx.symm⟩) = t
-      conv_lhs => rw [← hE_g (E.symm ⟨(t, x), hx.symm⟩), E.apply_symm_apply]
-    -- φ is surjective onto g⁻¹'{t}
-    have hφ_surj : ∀ y, y ∈ g ⁻¹' {t} → y ∈ Set.range φ := by
-      intro y hy
-      have hyt : g y = t := Set.mem_singleton_iff.mp hy
-      have hmk : (f y : ConnectedComponents X) = i t := by
-        rw [← hw y, hyt]
-      refine ⟨⟨f y, hmk⟩, ?_⟩
-      show E.symm ⟨(t, f y), hmk.symm⟩ = y
-      apply E.injective
-      simp only [Homeomorph.apply_symm_apply]
-      apply Subtype.ext
-      apply Prod.ext
-      · simp only [hE_g]; exact hyt.symm
-      · exact (hE_f y).symm
-    -- {x : X | mk x = i t} = connectedComponent (f y₀), which is preconnected.
-    have hit : i t = (f y₀ : ConnectedComponents X) := by rw [← hw y₀, hy₀t]
-    have hconn : IsPreconnected {x : X | (x : ConnectedComponents X) = i t} := by
-      suffices h : {x : X | (x : ConnectedComponents X) = i t} = connectedComponent (f y₀) by
-        rw [h]; exact isConnected_connectedComponent.isPreconnected
-      ext x
-      simp only [Set.mem_setOf_eq, hit]
-      exact ConnectedComponents.coe_eq_coe'
-    -- The fiber g⁻¹'{t} is the image of a preconnected set under φ, hence preconnected.
-    have heq : g ⁻¹' {t} = Set.range φ := by
-      ext y
-      simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_range]
-      exact ⟨fun hy => hφ_surj y hy, fun ⟨x, hx⟩ => hx ▸ hφ_img x⟩
-    -- The domain of φ has preconnected space.
-    have : PreconnectedSpace {x : X | (x : ConnectedComponents X) = i t} :=
-      Subtype.preconnectedSpace hconn
-    show IsPreconnected (g.toFun ⁻¹' {t})
-    rw [show g.toFun ⁻¹' {t} = Set.range φ from heq]
-    exact isPreconnected_range hφ_cont
-  · -- Surjectivity: for each t : T, find y : Y with g y = t, giving lift(mk y) = g y = t.
-    intro t
-    obtain ⟨x, hx⟩ := ConnectedComponents.surjective_coe (i t)
-    let y := pb.lift (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} t))
-      (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} x))
-      (by ext ⟨⟩; exact hx.symm) PUnit.unit
-    have hgy : g y = t := ConcreteCategory.congr_hom
-      (pb.lift_fst (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} t))
-        (TopCat.ofHom (ContinuousMap.const PUnit.{u+1} x))
-        (by ext ⟨⟩; exact hx.symm)) PUnit.unit
-    exact ⟨mk y, g.2.connectedComponentsLift_apply_coe y ▸ hgy⟩
+    Function.Bijective (connectedComponentsLift g.2) := sorry
 
 @[stacks 096C "first part"]
 theorem ConnectedComponents.isHomeomorph_lift_of_isPullback {Y T : Type u} [TopologicalSpace Y]

From bc5f85d2cb2464c8c2d81184b02d31b4a408503b Mon Sep 17 00:00:00 2001
From: "Christian Merten [bot]"
 <267582449+chrisflav-agent[bot]@users.noreply.github.com>
Date: Tue, 17 Mar 2026 17:02:37 +0000
Subject: [PATCH 9/9] style(Mathlib/Topology): move
 IsClosedMap.isClosed_singleton to a basic file about IsClosedMap

Move `IsClosedMap.isClosed_singleton` from `Proetale/Mathlib/Topology/Separation/Basic.lean`
to the more appropriate `Proetale/Mathlib/Topology/Maps/Basic.lean`, following the Mathlib
file structure where `IsClosedMap` is defined in `Mathlib.Topology.Maps.Basic`.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 Proetale.lean                                   |  1 +
 Proetale/Mathlib/Topology/Maps/Basic.lean       | 10 ++++++++++
 Proetale/Mathlib/Topology/Separation/Basic.lean | 10 +---------
 3 files changed, 12 insertions(+), 9 deletions(-)
 create mode 100644 Proetale/Mathlib/Topology/Maps/Basic.lean

diff --git a/Proetale.lean b/Proetale.lean
index 3994696..a8aadf9 100644
--- a/Proetale.lean
+++ b/Proetale.lean
@@ -72,6 +72,7 @@ import Proetale.Mathlib.Topology.Connected.TotallyDisconnected
 import Proetale.Mathlib.Topology.Constructions
 import Proetale.Mathlib.Topology.Inseparable
 import Proetale.Mathlib.Topology.JacobsonSpace
+import Proetale.Mathlib.Topology.Maps.Basic
 import Proetale.Mathlib.Topology.QuasiSeparated
 import Proetale.Mathlib.Topology.Separation.Basic
 import Proetale.Mathlib.Topology.Separation.Hausdorff
diff --git a/Proetale/Mathlib/Topology/Maps/Basic.lean b/Proetale/Mathlib/Topology/Maps/Basic.lean
new file mode 100644
index 0000000..ff80833
--- /dev/null
+++ b/Proetale/Mathlib/Topology/Maps/Basic.lean
@@ -0,0 +1,10 @@
+import Mathlib.Topology.Maps.Basic
+
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+
+/-- A closed map sends closed singletons to closed singletons. -/
+lemma IsClosedMap.isClosed_singleton {f : X → Y} (hf : IsClosedMap f)
+    {x : X} (hx : IsClosed {x}) :
+    IsClosed {f x} := by
+  rw [← Set.image_singleton]
+  exact hf _ hx
diff --git a/Proetale/Mathlib/Topology/Separation/Basic.lean b/Proetale/Mathlib/Topology/Separation/Basic.lean
index 2e94587..2b91d8b 100644
--- a/Proetale/Mathlib/Topology/Separation/Basic.lean
+++ b/Proetale/Mathlib/Topology/Separation/Basic.lean
@@ -1,13 +1,5 @@
 import Mathlib.Topology.Separation.Basic
-
-variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
-
-/-- A closed map sends closed singletons to closed singletons. -/
-lemma IsClosedMap.isClosed_singleton {f : X → Y} (hf : IsClosedMap f)
-    {x : X} (hx : IsClosed {x}) :
-    IsClosed {f x} := by
-  rw [← Set.image_singleton]
-  exact hf _ hx
+import Proetale.Mathlib.Topology.Maps.Basic
 
 /-- In a compact, T0 space every point specializes to a (not necessarily unique) closed point. -/
 lemma exists_isClosed_specializes {X : Type*} [TopologicalSpace X] [CompactSpace X]