The patch criterion for spectral spaces

A T0 topology generated by a family of clopen subsets of a compact space is spectral. This is the reusable criterion behind the spectrality of valuation spectra (Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 3.31): a compact witness topology t' on X together with a family U of t'-clopen sets generating a T0 topology t = generateFrom U produces a spectral space, and the members of U are quasi-compact opens of t.

The ambient TopologicalSpace X instance plays the role of the generated topology, pinned by the hypothesis t = generateFrom U in the style of TopologicalSpace.isTopologicalBasis_of_subbasis; the compact witness topology t' is an explicit second topology.

Main results

• TauCeti.spectralSpace_of_isClopen_generateFrom : Wedhorn's Proposition 3.31.
• TauCeti.isCompact_of_isClosed_generateFrom : every t'-closed set is quasi-compact for the generated topology, and TauCeti.isCompact_of_isClopen_generateFrom : in particular every member of U is.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Lemma 3.29 and Proposition 3.31.

theorem TauCeti.isCompact_generateFrom_of_isOpen {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} (hU : ∀ s ∈ U, IsOpen s) {s : Set X} (hs : IsCompact s) : IsCompact s

A set compact for t' is compact for the coarser topology generateFrom U generated by t'-open sets.

theorem TauCeti.compactSpace_of_isOpen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU' : ∀ s ∈ U, IsOpen s) : CompactSpace X

The generated topology of a compact presentation by open sets is compact; closedness of the generating sets is not needed for this component.

theorem TauCeti.isCompact_of_isClosed_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) {s : Set X} (hs : IsClosed s) : IsCompact s

Every set closed for the witness topology is quasi-compact for the generated topology. The two lemmas below are its instances, at a finite intersection of members of U and at a single member.

theorem TauCeti.isCompact_sInter_of_isClopen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) {f : Set (Set X)} (hf : f.Finite) (hfU : f ⊆ U) : IsCompact (⋂₀ f)

Every finite intersection of members of U is quasi-compact for the generated topology.

theorem TauCeti.isCompact_of_isClopen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) {s : Set X} (hs : s ∈ U) : IsCompact s

Every member of U is quasi-compact for the generated topology.

theorem TauCeti.prespectralSpace_of_isClopen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) : PrespectralSpace X

The generated topology of a compact patch presentation is prespectral.

theorem TauCeti.isClopen_of_isCompact_of_isOpen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hU : ∀ s ∈ U, IsClopen s) {V : Set X} (hV : IsCompact V) (hVo : IsOpen V) : IsClopen V

A set that is quasi-compact and open for the generated topology is clopen for the witness topology: it is a finite union of finite intersections of members of U. This is the bridge between the generated and witness topologies that the constructible-topology identification of a patch presentation consumes.

theorem TauCeti.quasiSeparatedSpace_of_isClopen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) : QuasiSeparatedSpace X

The generated topology of a compact patch presentation is quasi-separated.

theorem TauCeti.quasiSober_of_isClopen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) : QuasiSober X

The generated topology of a compact patch presentation is quasi-sober (Wedhorn, Lemma 3.29).

theorem TauCeti.spectralSpace_of_isClopen_generateFrom {X : Type u_1} {U : Set (Set X)} {t' : TopologicalSpace X} [t : TopologicalSpace X] (htU : t = TopologicalSpace.generateFrom U) (hcomp : CompactSpace X) (hU : ∀ s ∈ U, IsClopen s) [T0Space X] : SpectralSpace X

Wedhorn, Proposition 3.31 (Adic Spaces, arXiv:1910.05934v1): a T0 topology generated by a family of clopen subsets of a compact space is spectral.