A basis criterion for spectral maps, and transport of spectrality along an embedding

Two utilities for spectral spaces and maps. A continuous map is spectral as soon as the preimage of every member of some topological basis of the target is compact; and spectrality transports from the preimage of a set to the set itself along an embedding whose range contains it.

The basis criterion first. Spectrality asks for compact preimages of all compact open sets; the reduction to a basis is the observation that a compact open set is a finite union of basis elements — cover it by the basis members it contains and extract a finite subcover — and a finite union of compact preimages is compact.

Nothing is assumed of the basis members themselves, not even compactness: only their preimages enter the argument. In the intended applications the basis members are the distinguished quasi-compact opens of a spectral space (Wedhorn's family R for Spv (A, I)), whose preimages are computed by hand.

Mathlib's IsSpectralMap API provides constructors from identities, compositions and embeddings, but no criterion that tests spectrality on a basis; this supplies the missing entry point.

Main results

• TauCeti.isSpectralMap_of_isTopologicalBasis : a continuous map whose preimages of basis members are compact is a spectral map.
• TauCeti.spectralSpace_of_isEmbedding : a subset of the range of an embedding is spectral as soon as its preimage is — the transport step of any "prove it on a subspace" argument.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1 — Lemma 7.5(2) is the intended consumer of the basis criterion, and Corollary 7.12 and Theorem 7.35 of the transport lemma.

theorem TauCeti.isSpectralMap_of_isTopologicalBasis {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {B : Set (Set Y)} (hB : TopologicalSpace.IsTopologicalBasis B) (hf : Continuous f) (hpre : ∀ b ∈ B, IsCompact (f ⁻¹' b)) : IsSpectralMap f

A basis criterion for spectral maps. A continuous map is spectral as soon as the preimage of every member of a topological basis of the target is compact: a compact open set is a finite union of basis members, and a finite union of compact preimages is compact.

The basis members themselves need not be compact — only their preimages appear in the hypothesis.

theorem TauCeti.spectralSpace_of_isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) {S : Set Y} (hS : S ⊆ Set.range f) (h : SpectralSpace ↑(f ⁻¹' S)) : SpectralSpace ↑S

Spectrality transports from a trace along an embedding. A subset of the target contained in the range of an embedding is spectral as soon as its preimage is: the embedding restricts to a homeomorphism between the two.

This is the shape every "prove it on a subspace and carry it back" spectrality argument takes. It is worth stating separately because the reason one works on the subspace is usually that the inclusion is not a spectral map, which makes the general preservation theorems unavailable along it; this lemma supplies the homeomorphism route instead.