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.

class SpectralSpace (α : Type u_1) [TopologicalSpace α] extends T0Space α, CompactSpace α, QuasiSober α, QuasiSeparatedSpace α, PrespectralSpace α : 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 : α⦄ : Inseparable x y → x = y
• isCompact_univ : IsCompact Set.univ
• sober {S : Set α} : IsIrreducible S → IsClosed S → ∃ (x : α), IsGenericPoint x S
• inter_isCompact (U V : Set α) : IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
• isTopologicalBasis : TopologicalSpace.IsTopologicalBasis {U : Set α | IsOpen U ∧ IsCompact U}