Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.Basic

The underlying set of the adic spectrum Spa (A, A⁺) #

The set-level construction beneath Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.23.

For a subring A⁺ of a commutative ring A with a topology, spa A⁺ is the set of continuous points of Spv A that are sub-unit on A⁺:

spa A⁺ = {v ∈ cont A | v(a) ≤ 1 for every a ∈ A⁺}.

This is stated for arbitrary data — the file assumes [TopologicalSpace A] and nothing relating the topology to the ring operations, and asks nothing of the subring. It is Wedhorn's adic spectrum Spa (A, A⁺) under the hypotheses his Definition 7.23 carries: A a Huber ring (so in particular a topological ring, which is also what makes membership in cont A Wedhorn's Definition 7.7) and A⁺ a ring of integral elements. Those hypotheses enter only where theorems need them — spectrality (Wedhorn Theorem 7.35) is the first such theorem, and it lives with the Spv (A, I) machinery it consumes, not in this file. This mirrors how cont itself is defined below its Wedhorn hypotheses.

Following the roadmap's conventions, the plus ring is an explicit Subring A argument and the spectrum is a Set (Spv A), so a point is a valuation up to equivalence with no chosen value group, and the subspace topology is the one the coercion ↥(spa Aplus) carries. (Mathlib's in-flight SpaPoint of mathlib4#42315 instead bundles a representative valuation with a chosen value group — the representation the roadmap warns must be compared before later layers may use it; the subspace form here needs no such comparison.)

Main definitions #

Main results #

Provenance #

trivialSection_mem_spa_iff is the trivial-valuation witness of AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, project projects/AdicSpaces/, file Adic spaces/AdicSpectrum.lean, section Prop752, with the valuation-spectrum vocabulary adapted to this repository's Spv/ValuativeRel interface and the introduction direction strengthened to an equivalence. It reached this file by being factored out of TauCeti/AlgebraicGeometry/AdicSpace/Spa/Points.lean, which had used it inline.

References #

source
def TauCeti.ValuationSpectrum.spa {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) :
Set (ValuationSpectrum A)

The continuous points of Spv A that are sub-unit on the subring A⁺, as a Set (Spv A) — the subspace topology is the one the coercion ↥(spa Aplus) carries.

For a Huber ring A and a ring of integral elements A⁺ this is Wedhorn's adic spectrum Spa (A, A⁺) (Definition 7.23); the definition itself asks for neither — an arbitrary subring of an arbitrary commutative ring with a topology — and the Wedhorn hypotheses enter only in later theorems.

Equations
Instances For
    source
    theorem TauCeti.ValuationSpectrum.spa_def {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) :
    spa Aplus = cont A ∩ {v : ValuationSpectrum A | ∀ a ∈ Aplus, a ≤ᵥ 1}

    The set-level characterization of the adic spectrum: spa is the intersection of the continuous locus with the sub-unit locus of the plus ring. The definition is not exposed across the module boundary, so this equation is how consumers apply set-level results to spa — for instance spa_def ▸ Set.inter_subset_left : spa Aplus ⊆ cont A.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.mem_spa_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (v : ValuationSpectrum A) :
    v ∈ spa Aplus ↔ v.IsContinuous ∧ ∀ a ∈ Aplus, a ≤ᵥ 1

    Membership in the adic spectrum is continuity together with the sub-unit condition on the plus ring: v ∈ Spa (A, A⁺) iff v is continuous and v(a) ≤ 1 for every a ∈ A⁺.

    source
    theorem TauCeti.ValuationSpectrum.valuation_le_one_of_mem_spa {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {v : ValuationSpectrum A} (hv : v ∈ spa Aplus) {a : A} (ha : a ∈ Aplus) :
    v.valuation a ≤ 1

    At a point of Spa (A, A⁺), every element of the plus ring has valuation at most 1: the sub-unit condition of mem_spa_iff, read through the valuation v.valuation.

    source
    theorem TauCeti.ValuationSpectrum.spa_antitone {A : Type u_1} [CommRing A] [TopologicalSpace A] :
    Antitone spa

    Enlarging the plus ring shrinks the adic spectrum.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.spa_integralClosure {A : Type u_1} [CommRing A] [TopologicalSpace A] (R : Subring A) :
    spa (integralClosure (↥R) A).toSubring = spa R

    Replacing a subring by its integral closure does not change the sub-unit valuation locus.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.spa_topologicalClosure {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsSemitopologicalRing A] (S : Subring A) :
    spa S.topologicalClosure = spa S

    Replacing a subring by its topological closure does not change the adic spectrum: every point of Spa (A, A⁺) is already sub-unit on the closure of A⁺. This is the topological counterpart of spa_integralClosure.

    source
    theorem TauCeti.ValuationSpectrum.trivialSection_mem_spa_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (p : PrimeSpectrum A) :
    trivialSection p ∈ spa Aplus ↔ IsOpen ↑p.asIdeal

    The trivial valuation of a prime p is a point of the adic spectrum exactly when p is open, for any plus ring A⁺: the sub-unit condition holds at every element of A, since a trivial valuation takes only the values 0 and 1 and 1 lies outside a prime.

    source
    theorem TauCeti.ValuationSpectrum.spa_eq_empty_of_one_mem_closure_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousAdd A] (Aplus : Subring A) (h : 1 ∈ closure {0}) :
    spa Aplus = ∅

    The 1 ∈ closure {0} → Spa(A, A⁺) = ∅ half of Wedhorn Proposition 7.49(1). If 1 ∈ closure {0} in a commutative ring A with separately continuous addition, then Spa (A, A⁺) = ∅ for any plus ring A⁺.

    source
    theorem TauCeti.ValuationSpectrum.eq_top_of_spa_eq_empty {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousAdd A] (Aplus : Subring A) {I : Ideal A} (hI : IsOpen ↑I) (h : spa Aplus = ∅) :
    I = ⊤

    An empty adic spectrum forces every open ideal to be the unit ideal. A proper open ideal would lie in a maximal ideal, which is then open too, and the trivial valuation there would be a point of Spa (A, A⁺).

    This is the content of the converse half of Wedhorn Proposition 7.49(1); nothing about closure {0} is used, only that the ideal is open.