feat(Topology/Spectral/ConstructibleTopology): the constructible topology on a compact quasi-separated space X equals the topology generated by the constructible subsets of X

Mathlib.lean

@@ -8090,6 +8090,7 @@ public import Mathlib.Topology.Order.DenselyOrdered
 public import Mathlib.Topology.Order.ExtendFrom
 public import Mathlib.Topology.Order.ExtrClosure
 public import Mathlib.Topology.Order.Filter
+public import Mathlib.Topology.Order.GenerateFromLattice
 public import Mathlib.Topology.Order.Hom.Basic
 public import Mathlib.Topology.Order.Hom.Esakia
 public import Mathlib.Topology.Order.HullKernel

Mathlib/Order/BooleanSubalgebra.lean

@@ -379,6 +379,18 @@ lemma closure_bot_sup_induction {p : ∀ g ∈ closure s, Prop} (mem : ∀ x hx,
       compl_mem' := fun ⟨_, hb⟩ ↦ ⟨_, compl _ _ hb⟩ }
   closure_le (L := L).mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
 
+lemma closure_eq_latticeClosure (hs1 : ⊥ ∈ s) (hs2 : compl '' s = s) :
+    closure s = latticeClosure s := by
+  refine subset_antisymm ?_ latticeClosure_subset_closure
+  intro t ht
+  induction ht using closure_bot_sup_induction with
+  | mem _ hx => apply subset_latticeClosure hx
+  | bot => apply subset_latticeClosure hs1
+  | sup _ _ _ _ hx hy => apply isSublattice_latticeClosure.supClosed hx hy
+  | compl _ _ h =>
+    rw [← compl_image_latticeClosure_eq_of_compl_image_eq_self hs2]
+    exact mem_image_of_mem compl h
+
 section sdiff_sup
 
 variable (isSublattice : IsSublattice s) (bot_mem : ⊥ ∈ s) (top_mem : ⊤ ∈ s)

Mathlib/Topology/Order/GenerateFromLattice.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Fangming Li. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fangming Li
+-/
+module
+
+public import Mathlib.Order.SupClosed
+public import Mathlib.Topology.Order
+
+/-!
+# The topology generated by the lattice closure of a collection of sets
+
+In this file, we prove that for `α : Type*` and `s : Set (Set α)`, the topology on `α` generated
+by `latticeClosure s` is the same as the topology generated by `s`.
+-/
+
+@[expose] public section
+
+open TopologicalSpace
+
+lemma generateFrom_latticeClosure {α : Type*} (s : Set (Set α)) :
+    generateFrom (latticeClosure s) = generateFrom s := by
+  let : TopologicalSpace α := generateFrom s
+  refine le_antisymm (generateFrom_anti subset_latticeClosure) ?_
+  refine le_generateFrom fun o hos => ?_
+  induction hos using latticeClosure_sup_inf_induction with
+  | mem _ has => exact isOpen_generateFrom_of_mem has
+  | sup _ _ _ _ ha hb => exact ha.union hb
+  | inf _ _ _ _ ha hb => exact ha.inter hb

Mathlib/Topology/Spectral/ConstructibleTopology.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2025 Jiedong Jiang, Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Jiedong Jiang, Christian Merten
+Authors: Johan Commelin, Jiedong Jiang, Fangming Li, Christian Merten
 -/
 module
 
+public import Mathlib.Topology.Constructible
+public import Mathlib.Topology.Order.GenerateFromLattice
 public import Mathlib.Topology.Spectral.Basic
 public import Mathlib.Topology.WithTopology
 public import Mathlib.Topology.JacobsonSpace
@@ -47,7 +49,12 @@ def constructibleTopology (X : Type*) [TopologicalSpace X] : TopologicalSpace X
 abbrev WithConstructibleTopology (X : Type*) [TopologicalSpace X] : Type _ :=
   WithTopology X (constructibleTopology X)
 
-open Topology
+open TopologicalSpace Topology
+
+variable (X) in
+@[simp]
+lemma empty_mem_constructibleTopologySubbasis : ∅ ∈ constructibleTopologySubbasis X :=
+  Or.intro_left _ ⟨isOpen_empty, isCompact_empty⟩
 
 lemma WithConstructibleTopology.isOpen_iff {s : Set (WithConstructibleTopology X)} :
     IsOpen s ↔ IsOpen[constructibleTopology X] (WithTopology.toTopology _ ⁻¹' s) :=
@@ -72,6 +79,38 @@ lemma compl_mem_constructibleTopologySubbasis_iff {s : Set X} :
     sᶜ ∈ constructibleTopologySubbasis X ↔ s ∈ constructibleTopologySubbasis X := by
   grind [constructibleTopologySubbasis, isClosed_compl_iff, compl_compl]
 
+lemma compl_image_constructibleTopologySubbasis :
+    compl '' constructibleTopologySubbasis X = constructibleTopologySubbasis X := by
+  grind [constructibleTopologySubbasis, isClosed_compl_iff, compl_compl]
+
+lemma latticeClosure_constructibleTopologySubbasis [CompactSpace X] [QuasiSeparatedSpace X] :
+    latticeClosure (constructibleTopologySubbasis X) = { s | IsConstructible s } := by
+  rw [← BooleanSubalgebra.closure_eq_latticeClosure (empty_mem_constructibleTopologySubbasis X)
+      compl_image_constructibleTopologySubbasis]
+  dsimp only [IsConstructible, SetLike.setOf_mem_eq]
+  congr 1
+  refine le_antisymm ?_ (BooleanSubalgebra.closure_mono ?_)
+  · rw [BooleanSubalgebra.closure_le]
+    rintro s (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
+    · apply BooleanSubalgebra.subset_closure
+      grind [QuasiSeparatedSpace.isRetrocompact_iff_isCompact]
+    · rw [← compl_compl s]
+      refine BooleanSubalgebra.compl_mem (BooleanSubalgebra.subset_closure ?_)
+      grind [QuasiSeparatedSpace.isRetrocompact_iff_isCompact, IsClosed.isOpen_compl]
+  · grind [QuasiSeparatedSpace.isRetrocompact_iff_isCompact, constructibleTopologySubbasis]
+
+lemma constructibleTopologySubbasis_subset_isConstructible
+    [CompactSpace X] [QuasiSeparatedSpace X] :
+    constructibleTopologySubbasis X ⊆ { s | IsConstructible s } := by
+  simp [← latticeClosure_constructibleTopologySubbasis]
+
+variable (X) in
+lemma constructibleTopology_eq_generateFrom_isConstructible
+    [CompactSpace X] [QuasiSeparatedSpace X] :
+    constructibleTopology X = generateFrom { s | IsConstructible s } := by
+  rw [constructibleTopology, ← generateFrom_latticeClosure (constructibleTopologySubbasis X),
+    latticeClosure_constructibleTopologySubbasis]
+
 lemma isCompact_of_mem_constructibleTopologySubbasis [CompactSpace X] {s : Set X}
     (hs : s ∈ constructibleTopologySubbasis X) : IsCompact s := by
   obtain (hs | hs) := hs