Spectral spaces

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.

class SpectralSpace (X : Type u_3) [TopologicalSpace X] extends T0Space X, CompactSpace X, QuasiSober X, QuasiSeparatedSpace X, PrespectralSpace X : Prop

A topological space is spectral if it is T0, compact, sober, quasi-separated, and its compact open subsets form an open basis.

• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• isCompact_univ : IsCompact Set.univ
• sober {S : Set X} : IsIrreducible S → IsClosed S → ∃ (x : X), IsGenericPoint x S
• inter_isCompact (U V : Set X) : IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
• isTopologicalBasis : TopologicalSpace.IsTopologicalBasis {U : Set X | IsOpen U ∧ IsCompact U}

theorem Topology.IsOpenEmbedding.spectralSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [SpectralSpace Y] [CompactSpace X] (hf : IsOpenEmbedding f) : SpectralSpace X