Cont A is a spectral space: the second half of Wedhorn's Corollary 7.12

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Corollary 7.12.

The continuous points of the valuation spectrum of a Huber ring form a spectral space. Wedhorn draws this as a corollary of Theorem 7.10: Cont A is closed in Spv (A, IA), and a closed subspace of a spectral space is spectral.

The closedness half is TauCeti.ValuationSpectrum.isClosed_val_preimage_cont; this file draws the conclusion. A closed subset is in particular pro-constructible, hence spectral in the spectral space Spv (A, IA), so TauCeti.spectralSpace_of_isEmbedding carries it back along the subtype embedding, using the Theorem 7.10 inclusion Cont A ⊆ Spv (A, IA).

The argument is run on the subspace and transported back along a homeomorphism rather than carried out in Spv A, because the inclusion Spv (A, IA) → Spv A is not a spectral map (Remark 7.6) and the general preservation theorems are therefore unavailable along it.

Main results

• TauCeti.ValuationSpectrum.spectralSpace_cont_of_pairOfDefinition : Cont A is a spectral space, from an explicit pair of definition.
• The SpectralSpace (cont A) instance for a Huber ring, which names no pair.

theorem TauCeti.ValuationSpectrum.spectralSpace_cont_of_pairOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) : SpectralSpace ↑(cont A)

Wedhorn Corollary 7.12, the spectrality half, from an explicit pair of definition: the trace of Cont A on Spv (A, IA) is closed, hence pro-constructible, and Cont A is homeomorphic to that trace.

instance TauCeti.ValuationSpectrum.instSpectralSpaceElemContOfIsHuberRing {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] : SpectralSpace ↑(cont A)

Wedhorn Corollary 7.12: over a Huber ring the continuous points form a spectral space — by instance synthesis, with the pair of definition chosen from IsHuberRing.nonempty_pairOfDefinition, so that the statement mentions no pair. That the space does not depend on the pair is already true by construction: TauCeti.ValuationSpectrum.cont is defined from the topology of A alone.