feat: define spectral spaces and prove that a quasi-compact open of a spectral space is spectral (leanprover-community#11090)

Define spectral spaces and prove that a quasi-compact open of a spectral space is spectral.

Co-authored-by: Johan Commelin <johan@commelin.net>

Author: pangelinos

Mathlib/Topology/QuasiSeparated.lean

@@ -82,6 +82,11 @@ theorem IsQuasiSeparated.image_of_isEmbedding {s : Set α} (H : IsQuasiSeparated
     rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
     exact hV.trans (Set.image_subset_range _ _)
 
+theorem IsQuasiSeparated.of_subset {s t : Set α} (ht : IsQuasiSeparated t) (h : s ⊆ t) :
+    IsQuasiSeparated s := by
+  intro U V hU hU' hU'' hV hV' hV''
+  exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''
+
 theorem Topology.IsOpenEmbedding.isQuasiSeparated_iff (h : IsOpenEmbedding f) {s : Set α} :
     IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s) := by
   refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩
@@ -91,17 +96,17 @@ theorem Topology.IsOpenEmbedding.isQuasiSeparated_iff (h : IsOpenEmbedding f) {s
     H (f '' U) (f '' V) (image_mono hU) (h.isOpenMap _ hU') (hU''.image h.continuous)
       (image_mono hV) (h.isOpenMap _ hV') (hV''.image h.continuous)
 
+lemma Topology.IsOpenEmbedding.quasiSeparatedSpace [QuasiSeparatedSpace β] (h : IsOpenEmbedding f) :
+    QuasiSeparatedSpace α := by
+  rw [← isQuasiSeparated_univ_iff, h.isQuasiSeparated_iff]
+  exact isQuasiSeparated_univ.of_subset <| Set.subset_univ _
+
 theorem isQuasiSeparated_iff_quasiSeparatedSpace (s : Set α) (hs : IsOpen s) :
     IsQuasiSeparated s ↔ QuasiSeparatedSpace s := by
   rw [← isQuasiSeparated_univ_iff]
   convert (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm
   simp
 
-theorem IsQuasiSeparated.of_subset {s t : Set α} (ht : IsQuasiSeparated t) (h : s ⊆ t) :
-    IsQuasiSeparated s := by
-  intro U V hU hU' hU'' hV hV' hV''
-  exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''
-
 instance (priority := 100) T2Space.to_quasiSeparatedSpace [T2Space α] : QuasiSeparatedSpace α :=
   ⟨fun _ _ _ hU' _ hV' => hU'.inter hV'⟩
 

Mathlib/Topology/Spectral/Basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Fangming Li. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fangming Li
+Authors: Fangming Li, Panagiotis Angelinos
 -/
 module
 
@@ -13,16 +13,35 @@ public import Mathlib.Topology.Spectral.Prespectral
 
 A topological space is spectral if it is T0, compact, sober, quasi-separated, and its compact open
 subsets form an open basis. Prime spectra of commutative semirings are spectral spaces.
+
+## Main Results
+
+- `SpectralSpace` : Predicate for a topological space to be spectral.
+- `Topology.IsOpenEmbedding.spectralSpace` : a compact open subspace of a spectral space is spectral
+
+## References
+
+See [stacks-project], tag 08YF for details.
 -/
 
 @[expose] public section
 
-variable (α : Type*) [TopologicalSpace α]
+open Topology
+
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y}
 
 /--
 A topological space is spectral if it is T0, compact, sober, quasi-separated, and its compact open
 subsets form an open basis.
 -/
 @[stacks 08YG]
-class SpectralSpace : Prop extends
-  T0Space α, CompactSpace α, QuasiSober α, QuasiSeparatedSpace α, PrespectralSpace α
+class SpectralSpace (X : Type*) [TopologicalSpace X] : Prop extends
+  T0Space X, CompactSpace X, QuasiSober X, QuasiSeparatedSpace X, PrespectralSpace X
+
+theorem Topology.IsOpenEmbedding.spectralSpace
+    [SpectralSpace Y] [CompactSpace X] (hf : IsOpenEmbedding f) :
+    SpectralSpace X where
+  __ := hf.quasiSober
+  __ := hf.prespectralSpace
+  __ := hf.quasiSeparatedSpace
+  __ := hf.isEmbedding.t0Space

Mathlib/Topology/Spectral/Prespectral.lean

@@ -77,6 +77,21 @@ lemma PrespectralSpace.of_isClosedEmbedding [PrespectralSpace Y]
     (f : X → Y) (hf : IsClosedEmbedding f) : PrespectralSpace X :=
   .of_isInducing f hf.isInducing hf.isProperMap.isSpectralMap
 
+/-- Let `f : X → Y` be an open embedding of topological spaces.
+If `Y` is a prespectral space (i.e., the quasi-compact opens of `Y` form a basis),
+then `X` is also a prespectral space. -/
+lemma Topology.IsOpenEmbedding.prespectralSpace [PrespectralSpace Y]
+    {f : X → Y} (hf : IsOpenEmbedding f) :
+    PrespectralSpace X where
+  isTopologicalBasis := by
+    apply isTopologicalBasis_of_isOpen_of_nhds (fun U hU ↦ hU.1) <| fun x U hx hU ↦ ?_
+    obtain ⟨V, ⟨hoV, hcV⟩, hfx, hVf⟩ : ∃ V ∈ {V | IsOpen V ∧ IsCompact V}, f x ∈ V ∧ V ⊆ f '' U :=
+      (PrespectralSpace.isTopologicalBasis (X := Y)).isOpen_iff.mp
+        (hf.isOpen_iff_image_isOpen.mp hU) (f x) ⟨x, hx, rfl⟩
+    refine ⟨f ⁻¹' V, ⟨hoV.preimage hf.continuous, ?_⟩, ⟨hfx, fun y hy ↦ ?_⟩⟩
+    · exact hf.toIsInducing.isCompact_preimage' hcV <| Set.SurjOn.subset_range hVf
+    · exact hf.injective.mem_set_image.mp (hVf hy)
+
 instance PrespectralSpace.sigma {ι : Type*} (X : ι → Type*) [∀ i, TopologicalSpace (X i)]
     [∀ i, PrespectralSpace (X i)] : PrespectralSpace (Σ i, X i) :=
   .of_isTopologicalBasis (IsTopologicalBasis.sigma fun i ↦ isTopologicalBasis) fun U hU ↦ by