The patch presentation of the valuation spectrum

Following Wedhorn, Adic Spaces (arXiv:1910.05934v1), proof of Proposition 4.7: the map sending a point of Spv A to the boolean table of its relation embeds Spv A into the compact product (A × A) → Bool, with closed image; the basic opens of Spv A are clopen for the induced compact topology. This is the presentation that the patch criterion for spectral spaces consumes to prove Spv A spectral.

It also settles quasi-compactness of the generating family of Spv A, by instantiating the patch criterion's isCompact_of_isClosed_generateFrom at patchTopology A: the mechanism lives once, in TauCeti/Topology/Spectral/PatchCriterion.lean, and is specialised here. That is the part of Wedhorn's Theorem 4.9 which says the family consists of quasi-compact opens, as opposed to merely generating the topology. It says nothing about Lemma 7.5(1), whose family lives in Spv (A, I): these statements do not transfer to the traces along the inclusion. That side is proved separately in SpvOfIdeal/Spectral.lean, by the same criterion applied to the witness topology coinduced along r_I. Nor is the basis property proved here — only quasi-compactness of the individual members.

The quasi-compactness of the basic opens also yields, by stability of pro-constructibility under intersections, that the sub-unit locus {v | ∀ a ∈ S, v(a) ≤ 1} is pro-constructible in Spv A. Like everything above this is a statement about Spv A itself, subject to the same non-transfer caveat: the Spv (A, IA) analogue that Theorem 7.35 consumes is proved on that side (isProConstructible_val_preimage_setOfPred_forall_vle_one), not by restriction.

Main definitions

• TauCeti.ValuationSpectrum.toPatch : The relation table Spv A → (A × A) → Bool.
• TauCeti.ValuationSpectrum.patchTopology : The compact witness topology on Spv A induced from the product.

Main results

• TauCeti.ValuationSpectrum.isClosedEmbedding_toPatch : The table is a closed embedding of the witness topology into the product.
• TauCeti.ValuationSpectrum.compactSpace_patchTopology : The witness topology is compact.
• TauCeti.ValuationSpectrum.isClopen_patchTopology_basicOpen : Basic opens are clopen for the witness topology.
• TauCeti.ValuationSpectrum.isCompact_of_isClosed_patchTopology : a patch-closed subset is quasi-compact, with TauCeti.ValuationSpectrum.isCompact_basicOpen and TauCeti.ValuationSpectrum.isCompact_basicOpenFinset its two instances.
• TauCeti.ValuationSpectrum.isProConstructible_setOfPred_forall_vle_one : the locus v ≤ 1 on a set of ring elements is pro-constructible in Spv A — the Spv A-level shape of the sub-unit condition of Spa (A, A⁺); the Spv (A, IA) statement that Wedhorn's Theorem 7.35 consumes is isProConstructible_val_preimage_setOfPred_forall_vle_one (SpvOfIdeal/Spectral.lean), proved there since the inclusion is not spectral.

Provenance

The corresponding development in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, project projects/AdicSpaces/, reaches spectrality through isSpectralSpace_of_qcKolmogorov_oc_basis and Spv.isSpectralSpace, which return a CompactSpace ∧ T0Space ∧ QuasiSober conjunction; it has no counterpart to an isolated quasi-compactness statement about a single rational subset. Nothing was copied.

noncomputable def TauCeti.ValuationSpectrum.toPatch {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) : A × A → Bool

The relation table of a point of Spv A: the boolean function recording, for each pair (f, s), whether v(f) ≤ v(s).

Equations

• v.toPatch p = decide (p.1 ≤ᵥ p.2)

@[simp]

theorem TauCeti.ValuationSpectrum.toPatch_eq_true_iff {A : Type u_1} [CommRing A] (v : ValuationSpectrum A) (p : A × A) : v.toPatch p = true ↔ p.1 ≤ᵥ p.2

A coordinate of the relation table is true exactly when the relation holds there.

theorem TauCeti.ValuationSpectrum.toPatch_injective {A : Type u_1} [CommRing A] : Function.Injective toPatch

The relation table determines the point: toPatch is injective.

@[instance_reducible]

noncomputable def TauCeti.ValuationSpectrum.patchTopology (A : Type u_2) [CommRing A] : TopologicalSpace (ValuationSpectrum A)

The compact witness topology on Spv A: the topology induced from the product (A × A) → Bool of discrete factors along the relation table.

Equations

• TauCeti.ValuationSpectrum.patchTopology A = TopologicalSpace.induced TauCeti.ValuationSpectrum.toPatch inferInstance

theorem TauCeti.ValuationSpectrum.range_toPatch_eq {A : Type u_1} [CommRing A] : Set.range toPatch = {g : A × A → Bool | (∀ (x y : A), g (x, y) = true ∨ g (y, x) = true) ∧ (∀ (x y z : A), g (x, y) = true → g (y, z) = true → g (x, z) = true) ∧ (∀ (x y z : A), g (x, z) = true → g (y, z) = true → g (x + y, z) = true) ∧ (∀ (x y z : A), g (x, y) = true → g (x * z, y * z) = true) ∧ (∀ (x y z : A), g (z, 0) = false → g (x * z, y * z) = true → g (x, y) = true) ∧ g (1, 0) = false ∧ ∀ (x y : A), g (x * y, y * x) = true}

The range of the relation table is exactly the set of tables satisfying the ValuativeRel axioms pointwise.

theorem TauCeti.ValuationSpectrum.isClosed_range_toPatch {A : Type u_1} [CommRing A] : IsClosed (Set.range toPatch)

The range of the relation table is closed: each axiom of ValuativeRel is a closed condition on tables.

theorem TauCeti.ValuationSpectrum.isClosedEmbedding_toPatch {A : Type u_1} [CommRing A] : Topology.IsClosedEmbedding toPatch

The relation table is a closed embedding of the patch topology into the product.

theorem TauCeti.ValuationSpectrum.compactSpace_patchTopology {A : Type u_1} [CommRing A] : CompactSpace (ValuationSpectrum A)

The patch topology is compact: the table embeds Spv A as a closed subspace of a compact product.

theorem TauCeti.ValuationSpectrum.basicOpen_eq_toPatch_preimage {A : Type u_1} [CommRing A] (f s : A) : basicOpen f s = toPatch ⁻¹' {g : A × A → Bool | g (f, s) = true ∧ g (s, 0) = false}

A basic open is the table preimage of a two-coordinate condition.

theorem TauCeti.ValuationSpectrum.isClopen_patchTopology_basicOpen {A : Type u_1} [CommRing A] (f s : A) : IsClopen (basicOpen f s)

Basic opens are clopen for the patch topology.

instance TauCeti.ValuationSpectrum.instSpectralSpace {A : Type u_1} [CommRing A] : SpectralSpace (ValuationSpectrum A)

Spectrality of the valuation spectrum (Wedhorn, Adic Spaces, Theorem 4.9, via Propositions 4.7 and 3.31): the spectral topology of Spv A is generated by the basic opens, which are clopen for the compact patch topology, and is T0 — so Spv A is spectral by the patch criterion.

theorem TauCeti.ValuationSpectrum.isClopen_patchTopology_basicOpenFinset {A : Type u_1} [CommRing A] (T : Finset A) (s : A) : IsClopen (basicOpenFinset T s)

Spv(A)(T/s) is clopen for the patch topology: a finite intersection of patch-clopen basic opens. This is the input the patch criterion consumes.

Quasi-compactness of the rational subsets

theorem TauCeti.ValuationSpectrum.isCompact_of_isClosed_patchTopology {A : Type u_1} [CommRing A] {U : Set (ValuationSpectrum A)} (hU : IsClosed U) : IsCompact U

Any patch-closed subset of Spv A is quasi-compact — the patch criterion's isCompact_of_isClosed_generateFrom, instantiated at the patch presentation.

theorem TauCeti.ValuationSpectrum.isCompact_basicOpen {A : Type u_1} [CommRing A] (f s : A) : IsCompact (basicOpen f s)

A basic open of Spv A is quasi-compact.

theorem TauCeti.ValuationSpectrum.isCompact_basicOpenFinset {A : Type u_1} [CommRing A] (T : Finset A) (s : A) : IsCompact (basicOpenFinset T s)

Spv(A)(T/s) is quasi-compact: a finite intersection of patch-clopen basic opens is patch-clopen.

The sub-unit locus is pro-constructible

theorem TauCeti.ValuationSpectrum.isProConstructible_setOfPred_forall_vle_one {A : Type u_1} [CommRing A] (S : Set A) : IsProConstructible {v : ValuationSpectrum A | ∀ a ∈ S, a ≤ᵥ 1}

The locus v ≤ 1 on a set of ring elements is pro-constructible in Spv A.

At S = A⁺ this is the Spv A-level shape of the sub-unit condition cutting Spa (A, A⁺) out of Cont A (spa_def). Wedhorn's Theorem 7.35 consumes the corresponding statement in Spv (A, IA), which does not follow from this one by restriction — the inclusion Spv(A,I) → Spv A is not spectral — and is instead proved from the rational family as isProConstructible_val_preimage_setOfPred_forall_vle_one in SpvOfIdeal/Spectral.lean.