Pro-constructible subsets of a spectral space

A subset of a topological space is pro-constructible when it is closed for the constructible topology — the patch topology, generated by the quasi-compact opens and their complements. The name records the classical description of such a set on a spectral space: an intersection of finite unions of quasi-compact opens and complements of quasi-compact opens, that is, a filtered intersection of constructible sets.

The point of the notion is the theorem at the end of this file: a pro-constructible subspace of a spectral space is again spectral. This is how spectrality is transported to those subspaces of a valuation spectrum that adic geometry obtains by cutting: Cont A is closed in Spv(A,IA) and Spa(A,A⁺) is pro-constructible in it, and each inherits spectrality this way. Some such hypothesis is needed, since the naive statement — "a subspace of a spectral space is spectral" — is false. It is not a universal substitute either: Spv(A,I) is not obtained from Spv A by such a cut, since the inclusion Spv(A,I) → Spv A is not even a spectral map, and its spectrality is established by a separate retraction argument instead.

Implementation notes

IsProConstructible s is defined as closedness of the copy of s in Mathlib's type synonym WithConstructibleTopology X, so that typeclass inference has direct access to the instances carried by that topology — above all its compactness on a spectral space, which is the engine of every result below. TauCeti.isProConstructible_iff_isClosed is the same statement with the topology carried explicitly as IsClosed[constructibleTopology X] s.

Recall that Mathlib orders topologies by reverse inclusion of their open sets, so constructibleTopology X ≤ t says that the constructible topology is finer.

Main definitions

• TauCeti.IsProConstructible — s is closed for the constructible topology.

Main results

• TauCeti.IsOpen.isOpen_constructibleTopology — on a prespectral space the constructible topology refines the given one; hence IsClosed.isProConstructible.
• IsCompact.isProConstructible — a quasi-compact open subset is pro-constructible. It is in fact clopen for the constructible topology, which is what makes the two previous families interact.
• TauCeti.IsProConstructible.inter, .iInter, .sInter, .union, .iUnion — the calculus of pro-constructible subsets. Arbitrary intersections and finite unions are allowed.
• TauCeti.IsProConstructible.preimage — pro-constructibility is stable under preimage along a spectral map; TauCeti.IsProConstructible.prod and .pi — and under products when the ambient factors complementary to each projection are quasi-compact.
• TauCeti.IsProConstructible.isCompact — a pro-constructible subset of a spectral space is quasi-compact.
• TauCeti.IsProConstructible.mem_of_isGenericPoint — the generic point of the closure of a pro-constructible subset of a spectral space lies in that subset. This is the whole content of the sobriety half of the main theorem.
• TauCeti.IsProConstructible.spectralSpace — a pro-constructible subspace of a spectral space is spectral, together with TauCeti.IsProConstructible.isSpectralMap_subtypeVal: its inclusion is a spectral map. IsClosed.spectralSpace is the closed special case, the counterpart of Mathlib's Topology.IsOpenEmbedding.spectralSpace.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §3.
• The Stacks Project, tag 08YF.

The constructible topology refines the given topology

theorem TauCeti.IsOpen.isOpen_constructibleTopology {X : Type u_1} [tX : TopologicalSpace X] [PrespectralSpace X] {s : Set X} (hs : IsOpen s) : IsOpen s

On a prespectral space every open subset is open for the constructible topology: an open set is a union of quasi-compact opens, and those belong to the defining subbasis.

theorem TauCeti.IsOpen.isOpen_preimage_ofTopology {X : Type u_1} [tX : TopologicalSpace X] [PrespectralSpace X] {s : Set X} (hs : IsOpen s) : IsOpen (WithTopology.ofTopology ⁻¹' s)

The copy in WithConstructibleTopology X of an open subset of a prespectral space is open.

theorem TauCeti.continuous_ofTopology_withConstructibleTopology (X : Type u_1) [tX : TopologicalSpace X] [PrespectralSpace X] : Continuous WithTopology.ofTopology

On a prespectral space the identity map from the constructible topology to the given topology is continuous.

Pro-constructible subsets

def TauCeti.IsProConstructible {X : Type u_1} [tX : TopologicalSpace X] (s : Set X) : Prop

A subset of a topological space is pro-constructible if it is closed for the constructible topology. On a spectral space these are exactly the filtered intersections of constructible subsets, whence the name.

The definition is phrased through Mathlib's type synonym WithConstructibleTopology X; TauCeti.isProConstructible_iff_isClosed is the same statement with the topology explicit.

Equations

• TauCeti.IsProConstructible s = IsClosed (WithTopology.ofTopology ⁻¹' s)

theorem TauCeti.isProConstructible_iff_isClosed {X : Type u_1} [tX : TopologicalSpace X] {s : Set X} : IsProConstructible s ↔ IsClosed s

Pro-constructibility of s is closedness of s for the constructible topology of X, carried explicitly as IsClosed[constructibleTopology X] s rather than through the type synonym WithConstructibleTopology X used in the definition.

@[simp]

theorem TauCeti.isProConstructible_empty {X : Type u_1} [tX : TopologicalSpace X] : IsProConstructible ∅

@[simp]

theorem TauCeti.isProConstructible_univ {X : Type u_1} [tX : TopologicalSpace X] : IsProConstructible Set.univ

theorem TauCeti.IsProConstructible.inter {X : Type u_1} [tX : TopologicalSpace X] {s t : Set X} (hs : IsProConstructible s) (ht : IsProConstructible t) : IsProConstructible (s ∩ t)

theorem TauCeti.IsProConstructible.union {X : Type u_1} [tX : TopologicalSpace X] {s t : Set X} (hs : IsProConstructible s) (ht : IsProConstructible t) : IsProConstructible (s ∪ t)

theorem TauCeti.IsProConstructible.iUnion {X : Type u_1} [tX : TopologicalSpace X] {ι : Type u_3} [Finite ι] {f : ι → Set X} (hf : ∀ (i : ι), IsProConstructible (f i)) : IsProConstructible (⋃ (i : ι), f i)

A finite indexed union of pro-constructible subsets is pro-constructible.

theorem Set.Finite.isProConstructible_biUnion {X : Type u_1} [tX : TopologicalSpace X] {ι : Type u_3} {I : Set ι} {f : ι → Set X} (hI : I.Finite) (hf : ∀ i ∈ I, TauCeti.IsProConstructible (f i)) : TauCeti.IsProConstructible (⋃ i ∈ I, f i)

A union of pro-constructible subsets over a finite set is pro-constructible.

theorem Finset.isProConstructible_biUnion {X : Type u_1} [tX : TopologicalSpace X] {ι : Type u_3} (I : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ I, TauCeti.IsProConstructible (f i)) : TauCeti.IsProConstructible (⋃ i ∈ I, f i)

A union of pro-constructible subsets over a finset is pro-constructible.

theorem TauCeti.IsProConstructible.iInter {X : Type u_1} [tX : TopologicalSpace X] {ι : Sort u_3} {f : ι → Set X} (hf : ∀ (i : ι), IsProConstructible (f i)) : IsProConstructible (⋂ (i : ι), f i)

theorem TauCeti.IsProConstructible.biInter {X : Type u_1} [tX : TopologicalSpace X] {ι : Sort u_3} {p : ι → Prop} {f : (i : ι) → p i → Set X} (hf : ∀ (i : ι) (hi : p i), IsProConstructible (f i hi)) : IsProConstructible (⋂ (i : ι), ⋂ (hi : p i), f i hi)

theorem TauCeti.IsProConstructible.sInter {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (hS : ∀ s ∈ S, IsProConstructible s) : IsProConstructible (⋂₀ S)

theorem IsCompact.isProConstructible {X : Type u_1} [tX : TopologicalSpace X] {s : Set X} (hcomp : IsCompact s) (hopen : IsOpen s) : TauCeti.IsProConstructible s

A quasi-compact open subset is pro-constructible: it is even clopen for the constructible topology, since it and its complement both belong to the defining subbasis.

theorem IsClosed.isProConstructible {X : Type u_1} [tX : TopologicalSpace X] [PrespectralSpace X] {s : Set X} (hs : IsClosed s) : TauCeti.IsProConstructible s

A closed subset of a prespectral space is pro-constructible.

Functoriality

theorem TauCeti.IsSpectralMap.continuous_constructibleTopology {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (hf : IsSpectralMap f) : Continuous f

A spectral map is continuous for the constructible topologies: it pulls the defining subbasis back into itself.

theorem TauCeti.IsProConstructible.preimage {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} {s : Set Y} (hs : IsProConstructible s) (hf : IsSpectralMap f) : IsProConstructible (f ⁻¹' s)

Pro-constructible subsets pull back along spectral maps.

theorem TauCeti.isSpectralMap_eval {ι : Type u_3} {Z : ι → Type u_4} [(i : ι) → TopologicalSpace (Z i)] (i : ι) (hZ : ∀ (j : ι), j ≠ i → IsCompact Set.univ) : IsSpectralMap fun (f : (i : ι) → Z i) => f i

Evaluation at a coordinate i is a spectral map as soon as every other factor is quasi-compact: the preimage of a quasi-compact open is a box with that set in the i-th slot and the whole space elsewhere, so only those other slots need a compactness hypothesis.

theorem TauCeti.IsProConstructible.prod {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [CompactSpace X] [CompactSpace Y] {s : Set X} {t : Set Y} (hs : IsProConstructible s) (ht : IsProConstructible t) : IsProConstructible (s ×ˢ t)

A product of two pro-constructible subsets in compact ambient spaces is pro-constructible.

theorem TauCeti.IsProConstructible.pi {ι : Type u_3} {Z : ι → Type u_4} [(i : ι) → TopologicalSpace (Z i)] {s : (i : ι) → Set (Z i)} (hZ : ∀ (i j : ι), j ≠ i → IsCompact Set.univ) (hs : ∀ (i : ι), IsProConstructible (s i)) : IsProConstructible (Set.univ.pi s)

A product of a family of pro-constructible subsets is pro-constructible when, for each coordinate, every other ambient factor is quasi-compact.

Pro-constructible subspaces of a spectral space

theorem TauCeti.IsProConstructible.isCompact {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : IsCompact s

A pro-constructible subset of a spectral space is quasi-compact: it is closed in the constructible topology, which is compact.

theorem TauCeti.IsProConstructible.mem_of_isGenericPoint {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) {η : X} (hη : IsGenericPoint η (closure s)) : η ∈ s

The key sobriety step. If s is pro-constructible in a spectral space and η is a generic point of the closure of s, then η ∈ s.

The quasi-compact open neighbourhoods of η form a filtered family — this is quasi-separatedness — and each meets s because η adheres to s. The traces s ∩ U are closed for the constructible topology, so patch compactness produces a common point ζ ∈ s of all of them. Then ζ lies in every quasi-compact open neighbourhood of η, that is η ∈ closure {ζ}, while ζ ∈ s gives closure {ζ} ⊆ closure s = closure {η}. The two points are therefore topologically indistinguishable, hence equal.

theorem TauCeti.IsProConstructible.isSpectralMap_subtypeVal {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : IsSpectralMap Subtype.val

The inclusion of a pro-constructible subset of a spectral space is a spectral map: the trace on it of a quasi-compact open is again pro-constructible, hence quasi-compact.

theorem TauCeti.IsProConstructible.compactSpace {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : CompactSpace ↑s

A pro-constructible subspace of a spectral space is quasi-compact.

theorem TauCeti.IsProConstructible.prespectralSpace {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : PrespectralSpace ↑s

A pro-constructible subspace of a spectral space has a basis of quasi-compact opens: the traces of the quasi-compact opens of the ambient space.

theorem TauCeti.IsProConstructible.quasiSeparatedSpace {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : QuasiSeparatedSpace ↑s

A pro-constructible subspace of a spectral space is quasi-separated: on the basis of traces of quasi-compact opens, quasi-separatedness is inherited from the ambient space.

theorem TauCeti.IsProConstructible.quasiSober {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : QuasiSober ↑s

A pro-constructible subspace of a spectral space is sober. An irreducible closed subset Z of it has irreducible image in the ambient space, whose closure has a generic point η; the image of Z is pro-constructible, so η lies in it by TauCeti.IsProConstructible.mem_of_isGenericPoint, and its preimage generates Z.

theorem TauCeti.IsProConstructible.spectralSpace {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsProConstructible s) : SpectralSpace ↑s

A pro-constructible subspace of a spectral space is spectral.

This is the transport principle behind the spectrality of Cont A and of Spa(A,A⁺) in adic geometry: both are obtained by cutting a space already known to be spectral along a pro-constructible condition. Spv(A,I) is not of this form and is handled separately.

theorem IsClosed.spectralSpace {X : Type u_1} [tX : TopologicalSpace X] [SpectralSpace X] {s : Set X} (hs : IsClosed s) : SpectralSpace ↑s

A closed subspace of a spectral space is spectral. Mathlib has the open counterpart, Topology.IsOpenEmbedding.spectralSpace; this is the closed one.