6. The adic spectrum🔗

Definition6.1

Statement uses 2

Statement dependency previews

Preview

Definition 4.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 7

Reverse dependency previews

Preview

Theorem 6.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Let (A, A^{+}) be an affinoid ring (Definition 5.1). The adic spectrum is the set of continuous valuations bounded by 1 on A^{+}: \mathrm{Spa}(A, A^{+}) = \{\, v \in \mathrm{Cont}(A) : v(f) \le 1 \text{ for all } f \in A^{+} \,\} (Definition 4.5). In Adic-Spaces: \texttt{Spa} (with the integral subring packaged by the class \texttt{PlusSubring}). This is the fundamental functor of Huber's theory. Following Wedhorn Definition 7.23.

Lean code for Definition6.1●2 definitions

defdefined in «Adic spaces»/AdicSpectrum.lean

complete

def ValuationSpectrum.Spa.{u_2} (A : Type u_2) [CommRing A]
  [TopologicalSpace A] (Aplus : Subring A) : Set (Spv A)

def ValuationSpectrum.Spa.{u_2} (A : Type u_2)
  [CommRing A] [TopologicalSpace A]
  (Aplus : Subring A) : Set (Spv A)

The *adic spectrum* `Spa(A, A⁺)` (Definition 7.23 of Wedhorn).

class(1 method)defined in «Adic spaces»/AdicSpectrum.lean

complete

class ValuationSpectrum.PlusSubring.{u_1} (A : Type u_1) [CommRing A] :
  Type u_1

class ValuationSpectrum.PlusSubring.{u_1}
  (A : Type u_1) [CommRing A] : Type u_1

A commutative ring equipped with a designated subring `A⁺`.

Methods

toSubring : Subring A

The subring of integral elements `A⁺`.

Theorem6.2

Statement uses 2

Statement dependency previews

Preview

Definition 4.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

A continuous homomorphism \varphi : A \to B of affinoid rings with A^{+} \subseteq \varphi^{-1}(B^{+}) induces a continuous map \mathrm{Spa}(B, B^{+}) \to \mathrm{Spa}(A, A^{+}) (\texttt{spaComap}), making \mathrm{Spa} a functor (Definition 6.1, Definition 4.2). Following Wedhorn Definition 7.23ff.

Lean code for Theorem6.2●2 declarations

defdefined in «Adic spaces»/AdicSpectrum.lean

complete

def ValuationSpectrum.spaComap.{u_1, u_2} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] {B : Type u_2}
  [CommRing B] [TopologicalSpace B] [ValuationSpectrum.PlusSubring B]
  {φ : A →+* B} (hφ : Continuous ⇑φ)
  (hAB :
    ValuationSpectrum.ringPlus A ≤
      Subring.comap φ (ValuationSpectrum.ringPlus B)) :
  C(↑(ValuationSpectrum.Spa B (ValuationSpectrum.ringPlus B)),
    ↑(ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A)))

def ValuationSpectrum.spaComap.{u_1, u_2}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  {B : Type u_2} [CommRing B]
  [TopologicalSpace B]
  [ValuationSpectrum.PlusSubring B]
  {φ : A →+* B} (hφ : Continuous ⇑φ)
  (hAB :
    ValuationSpectrum.ringPlus A ≤
      Subring.comap φ
        (ValuationSpectrum.ringPlus B)) :
  C(↑(ValuationSpectrum.Spa B
        (ValuationSpectrum.ringPlus B)),
    ↑(ValuationSpectrum.Spa A
        (ValuationSpectrum.ringPlus A)))

The continuous map `Spa(φ)` (Remark 7.28).

theoremdefined in «Adic spaces»/AdicSpectrum.lean

complete

theorem ValuationSpectrum.comap_mem_spa.{u_1, u_2} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] {B : Type u_2}
  [CommRing B] [TopologicalSpace B] [ValuationSpectrum.PlusSubring B]
  {φ : A →+* B} (hφ : Continuous ⇑φ)
  (hAB :
    ValuationSpectrum.ringPlus A ≤
      Subring.comap φ (ValuationSpectrum.ringPlus B))
  {v : Spv B}
  (hv : v ∈ ValuationSpectrum.Spa B (ValuationSpectrum.ringPlus B)) :
  ValuationSpectrum.comap φ v ∈
    ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A)

theorem ValuationSpectrum.comap_mem_spa.{u_1, u_2}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  {B : Type u_2} [CommRing B]
  [TopologicalSpace B]
  [ValuationSpectrum.PlusSubring B]
  {φ : A →+* B} (hφ : Continuous ⇑φ)
  (hAB :
    ValuationSpectrum.ringPlus A ≤
      Subring.comap φ
        (ValuationSpectrum.ringPlus B))
  {v : Spv B}
  (hv :
    v ∈
      ValuationSpectrum.Spa B
        (ValuationSpectrum.ringPlus B)) :
  ValuationSpectrum.comap φ v ∈
    ValuationSpectrum.Spa A
      (ValuationSpectrum.ringPlus A)

`Spa(φ)` via `comap` (Remark 7.28).

Proof for Theorem 6.2

uses 0

The valuation-spectrum comap \mathrm{Spv}(\varphi) is already continuous. If v \in \mathrm{Spa}(B,B^{+}) then v is continuous, so its pullback is continuous (\varphi being continuous); and for f \in A^{+} we have \varphi(f) \in B^{+}, whence (\varphi^*v)(f) = v(\varphi f) \le 1. Thus \varphi^* v \in \mathrm{Spa}(A,A^{+}), and restricting \mathrm{Spv}(\varphi) gives the required continuous map. Following Wedhorn Definition 7.23ff.

Theorem6.3

Statement uses 3

Statement dependency previews

Preview

Definition 1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

The adic spectrum \mathrm{Spa}(A, A^{+}) is quasi-compact (Definition 6.1, Theorem 4.4). In Adic-Spaces this is proved for Tate rings with an explicit pseudo-uniformiser (\texttt{isCompact\_spa\_of\_tate\_pseudouniformizer}, Definition 1.2) and for the discrete case (\texttt{instCompactSpace\_spa}). Following Wedhorn Theorem 7.30.

Lean code for Theorem6.3●2 theorems

theoremdefined in «Adic spaces»/SpaCompact.lean

complete

theorem ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer.{u_1}
  {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
  [ValuationSpectrum.PlusSubring A] (P : PairOfDefinition A)
  (hA₀_le : P.A₀ ≤ ValuationSpectrum.ringPlus A) (π : ↥P.A₀)
  (hI : P.I = Ideal.span {π})
  (hπ_tn : IsTopologicallyNilpotent (P.A₀.subtype π))
  (hπ_unit : IsUnit (P.A₀.subtype π))
  (hArch :
    ∀ (v : Spv A), MulArchimedean (ValuativeRel.ValueGroupWithZero A)) :
  IsCompact (ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A))

theorem ValuationSpectrum.isCompact_spa_of_tate_pseudouniformizer.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  [ValuationSpectrum.PlusSubring A]
  (P : PairOfDefinition A)
  (hA₀_le :
    P.A₀ ≤ ValuationSpectrum.ringPlus A)
  (π : ↥P.A₀) (hI : P.I = Ideal.span {π})
  (hπ_tn :
    IsTopologicallyNilpotent
      (P.A₀.subtype π))
  (hπ_unit : IsUnit (P.A₀.subtype π))
  (hArch :
    ∀ (v : Spv A),
      MulArchimedean
        (ValuativeRel.ValueGroupWithZero
          A)) :
  IsCompact
    (ValuationSpectrum.Spa A
      (ValuationSpectrum.ringPlus A))

**Compactness of `Spa A A⁺` for Tate rings with a pseudo-uniformizer**
(Wedhorn Theorem 7.30, Tate case). Under the hypotheses:

* a pair of definition `P` with `P.A₀ ⊆ A⁺`,
* `π ∈ P.A₀` is a topologically nilpotent unit in `A` (a pseudo-uniformizer),
* `P.I = (π)` (principal ideal of definition),
* MulArchimedean on the ValueGroup of every `v : Spv A`,

the adic spectrum `Spa(A, A⁺)` is quasi-compact in `Spv A`.

theoremdefined in «Adic spaces»/SpaCompact.lean

complete

theorem ValuationSpectrum.instCompactSpace_spa.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A]
  [DiscreteTopology A] :
  CompactSpace ↑(ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A))

theorem ValuationSpectrum.instCompactSpace_spa.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  [DiscreteTopology A] :
  CompactSpace
    ↑(ValuationSpectrum.Spa A
        (ValuationSpectrum.ringPlus A))

**T-NULL-0c capstone: `CompactSpace ↥(Spa(A, A⁺))` (discrete case).**

The adic spectrum `Spa(A, A⁺)` of a commutative ring `A` with the discrete
topology and a choice of integral subring `A⁺` is a compact topological space.

This is the discrete specialisation of Wedhorn Theorem 7.30. Together with
`ValuationSpectrum.instCompactSpace` (quasi-compactness of `Spv A`) it unblocks
the Nullstellensatz refinement / Cor 7.32 route to the dominating-unit lemma
(see `docs/plans/2026-04-16-s3-nullstellensatz-plan.md`, T-NULL-0c).

Proof for Theorem 6.3

uses 1

\mathrm{Spa}(A,A^{+}) sits inside the quasi-compact \mathrm{Spv}(A) (Theorem 4.4) as the locus of continuous valuations with v(f) \le 1 for f \in A^{+}. Each such condition is closed in the characteristic-function embedding, and a pseudo-uniformiser controls the value groups uniformly so the continuity locus is also closed. A closed subset of the compact product is compact, giving quasi-compactness of \mathrm{Spa}. Following Wedhorn Theorem 7.30.

Theorem6.4

Statement uses 2

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

When A^{\circ\circ} is open, every maximal ideal of A is open (Theorem 2.4, Definition 2.1): topologically nilpotent elements lie in every maximal ideal (\texttt{mem\_of\_isMaximal}), and the open-ideal criterion then makes the maximal ideal open (\texttt{isOpen\_of\_isMaximal\_of\_isOpen\_topologicallyNilpotent}). Following Wedhorn Proposition 7.51.

Lean code for Theorem6.4●2 theorems

theoremdefined in «Adic spaces»/AdicSpectrum.lean

complete

theorem IsTopologicallyNilpotent.mem_of_isMaximal.{u_1} {A : Type u_1}
  [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A]
  [IsTopologicalRing A] [IsUniformAddGroup A] [NonarchimedeanAddGroup A]
  [IsLinearTopology A A] {a : A} (ha : IsTopologicallyNilpotent a)
  (𝔪 : Ideal A) [𝔪.IsMaximal] : a ∈ 𝔪

theorem IsTopologicallyNilpotent.mem_of_isMaximal.{u_1}
  {A : Type u_1} [CommRing A]
  [UniformSpace A] [T2Space A]
  [CompleteSpace A] [IsTopologicalRing A]
  [IsUniformAddGroup A]
  [NonarchimedeanAddGroup A]
  [IsLinearTopology A A] {a : A}
  (ha : IsTopologicallyNilpotent a)
  (𝔪 : Ideal A) [𝔪.IsMaximal] : a ∈ 𝔪

Topologically nilpotent elements lie in every maximal ideal.

theoremdefined in «Adic spaces»/AdicSpectrum.lean

complete

theorem isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent.{u_1}
  {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A]
  [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A]
  [NonarchimedeanAddGroup A] [IsLinearTopology A A]
  (hopen : IsOpen {a | IsTopologicallyNilpotent a}) (𝔪 : Ideal A)
  [𝔪.IsMaximal] : IsOpen ↑𝔪

theorem isOpen_of_isMaximal_of_isOpen_topologicallyNilpotent.{u_1}
  {A : Type u_1} [CommRing A]
  [UniformSpace A] [T2Space A]
  [CompleteSpace A] [IsTopologicalRing A]
  [IsUniformAddGroup A]
  [NonarchimedeanAddGroup A]
  [IsLinearTopology A A]
  (hopen :
    IsOpen
      {a | IsTopologicallyNilpotent a})
  (𝔪 : Ideal A) [𝔪.IsMaximal] : IsOpen ↑𝔪

Every maximal ideal is open when `A°°` is open.

Proof for Theorem 6.4

uses 1

A topologically nilpotent t has 1 - t invertible, so t lies in the Jacobson radical, hence in every maximal ideal \mathfrak m; thus A^{\circ\circ} \subseteq \mathfrak m \subseteq \sqrt{\mathfrak m}. By the open-ideal criterion (Theorem 2.4) the containment A^{\circ\circ} \subseteq \sqrt{\mathfrak m} makes \mathfrak m open. Following Wedhorn Proposition 7.51.

Theorem6.5

uses 1used by 0✓L∃∀N

Every open maximal ideal \mathfrak m is the support of a point of \mathrm{Spa}(A, A^{+}) (Definition 6.1): the trivial valuation on the residue field A/\mathfrak m pulls back to a continuous, A^{+}-bounded valuation with support exactly \mathfrak m. Following Wedhorn Proposition 7.51.

Lean code for Theorem6.5●2 theorems

theoremdefined in «Adic spaces»/AdicSpectrum.lean

complete

theorem ValuationSpectrum.exists_mem_spa_supp_eq.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [ValuationSpectrum.PlusSubring A]
  (𝔪 : Ideal A) [𝔪.IsMaximal] (h𝔪 : IsOpen ↑𝔪) :
  ∃ v ∈ ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A),
    v.supp = 𝔪

theorem ValuationSpectrum.exists_mem_spa_supp_eq.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A]
  (𝔪 : Ideal A) [𝔪.IsMaximal]
  (h𝔪 : IsOpen ↑𝔪) :
  ∃
    v ∈
      ValuationSpectrum.Spa A
        (ValuationSpectrum.ringPlus A),
    v.supp = 𝔪

The trivial valuation on `A/𝔪` gives a point of `Spa(A, A⁺)`
with support `𝔪` (Prop 7.51).

theoremdefined in «Adic spaces»/AdicSpectrum.lean

complete

theorem ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent.{u_1}
  {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A]
  [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A]
  [NonarchimedeanAddGroup A] [IsLinearTopology A A]
  [ValuationSpectrum.PlusSubring A]
  (hopen : IsOpen {a | IsTopologicallyNilpotent a}) (𝔪 : Ideal A)
  [𝔪.IsMaximal] :
  ∃ v ∈ ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A),
    v.supp = 𝔪

theorem ValuationSpectrum.exists_mem_spa_supp_eq_of_isOpen_topologicallyNilpotent.{u_1}
  {A : Type u_1} [CommRing A]
  [UniformSpace A] [T2Space A]
  [CompleteSpace A] [IsTopologicalRing A]
  [IsUniformAddGroup A]
  [NonarchimedeanAddGroup A]
  [IsLinearTopology A A]
  [ValuationSpectrum.PlusSubring A]
  (hopen :
    IsOpen
      {a | IsTopologicallyNilpotent a})
  (𝔪 : Ideal A) [𝔪.IsMaximal] :
  ∃
    v ∈
      ValuationSpectrum.Spa A
        (ValuationSpectrum.ringPlus A),
    v.supp = 𝔪

Prop 7.51 with f-adic hypotheses.

Proof for Theorem 6.5

uses 0

Since \mathfrak m is maximal, A/\mathfrak m is a field; take the trivial valuation \mathbf 1 on it and set v = \mathbf 1 \circ \pi for \pi : A \to A/\mathfrak m. Then \mathrm{supp}(v) = \mathfrak m. For continuity, \{a : v(a) < \gamma\} is either \varnothing, all of A, or \mathfrak m (open by hypothesis), so all sublevel sets are open. As v takes values in \{0,1\} it is bounded by 1 on all of A, in particular on A^{+}, so v \in \mathrm{Spa}(A,A^{+}). Following Wedhorn Proposition 7.51.

Theorem6.6

Statement uses 3

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

For a non-open prime \mathfrak p there is a point of \mathrm{Spa}(A, A^{+}) whose support contains \mathfrak p (Definition 6.1, Definition 1.1), constructed by extending a valuation along a convex coarsening (Definition 4.7). In Adic-Spaces: \texttt{exists\_mem\_spa\_supp\_ge\_of\_nonOpen\_prime}. Following Wedhorn Lemma 7.45.

Lean code for Theorem6.6●1 theorem

theoremdefined in «Adic spaces»/Lemma745.lean

complete

theorem PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime.{u_1}
  {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
  (P : PairOfDefinition A) [IsAdicComplete P.I ↥P.A₀]
  [ValuationSpectrum.PlusSubring A] {𝔭 : Ideal A} [𝔭.IsPrime]
  (h𝔭 : ¬IsOpen ↑𝔭)
  (hAplus_le_A₀ : ↑(ValuationSpectrum.ringPlus A) ⊆ ↑P.A₀) :
  ∃ v ∈ ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A),
    𝔭 ≤ v.supp ∧ ¬P.idealOfDefinition ≤ v.supp

theorem PairOfDefinition.exists_mem_spa_supp_ge_of_nonOpen_prime.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  (P : PairOfDefinition A)
  [IsAdicComplete P.I ↥P.A₀]
  [ValuationSpectrum.PlusSubring A]
  {𝔭 : Ideal A} [𝔭.IsPrime]
  (h𝔭 : ¬IsOpen ↑𝔭)
  (hAplus_le_A₀ :
    ↑(ValuationSpectrum.ringPlus A) ⊆
      ↑P.A₀) :
  ∃
    v ∈
      ValuationSpectrum.Spa A
        (ValuationSpectrum.ringPlus A),
    𝔭 ≤ v.supp ∧
      ¬P.idealOfDefinition ≤ v.supp

**Lemma 7.45 of Wedhorn.** Non-open primes are supports in `Spa`.

Given a complete affinoid ring `(A, A⁺)` with pair of definition `(A₀, I)` and
a non-open prime `𝔭` of `A`, there exists `v ∈ Spa(A, A⁺)` with `supp(v) ⊇ 𝔭`.

Note: Wedhorn's Lemma 7.45 gives `supp ⊇ 𝔭` (not `= 𝔭`) in the general case.
The exact equality `supp = 𝔭` requires the rank-1 domination theorem (Bourbaki)
or the discrete topology case (already proved in `AdicSpectrum.lean`).

The proof uses `restrictToConvex` with `convexGenerated` to produce a continuous
valuation. The cofinal property of `convexGenerated` gives continuity directly,
avoiding the `MulArchimedean` intermediate.

References: Wedhorn, Adic Spaces, Lemma 7.45.

Proof for Theorem 6.6

uses 0

Because \mathfrak p is not open, the defining ideal I is not contained in \sqrt{\mathfrak p}, so some u \in I escapes \mathfrak p. Building a valuation on A/\mathfrak p with u cofinal and restricting to the convex subgroup generated by its values (\texttt{restrictToConvex}) yields a continuous valuation, bounded by 1 on A^{+}, whose support dominates \mathfrak p. This is a point of \mathrm{Spa}(A,A^{+}) with the desired support. Following Wedhorn Lemma 7.45.

Theorem6.7

Statement uses 2

Statement dependency previews

Preview

Definition 1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

(Corollary 7.32.) Over a Tate ring, given finitely many f_i and a pseudo-uniformiser context, there is a unit (a power of the uniformiser) that dominates all the f_i on the quasi-compact \mathrm{Spa} (Theorem 6.3, Definition 1.2). In Adic-Spaces: \texttt{exists\_dominating\_unit}. This denominator-clearing step is the engine of the rational-cover refinements. Following Wedhorn Corollary 7.32.

Lean code for Theorem6.7●1 theorem

theoremdefined in «Adic spaces»/Cor732.lean

complete

theorem ValuationSpectrum.exists_dominating_unit.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
  [ValuationSpectrum.PlusSubring A] (P : PairOfDefinition A)
  (hA₀_le : P.A₀ ≤ ValuationSpectrum.ringPlus A) (π : ↥P.A₀)
  (hI : P.I = Ideal.span {π})
  (hπ_tn : IsTopologicallyNilpotent (P.A₀.subtype π))
  (hπ_unit : IsUnit (P.A₀.subtype π))
  (hArch :
    ∀ (v : Spv A), MulArchimedean (ValuativeRel.ValueGroupWithZero A))
  (T : Finset A)
  (hT :
    ∀ v ∈ ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A),
      ∃ t ∈ T, ¬t ≤ᵥ 0) :
  ∃ s,
    ∀ v ∈ ValuationSpectrum.Spa A (ValuationSpectrum.ringPlus A),
      ∃ t ∈ T, ↑s ≤ᵥ t ∧ ¬t ≤ᵥ ↑s

theorem ValuationSpectrum.exists_dominating_unit.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  [ValuationSpectrum.PlusSubring A]
  (P : PairOfDefinition A)
  (hA₀_le :
    P.A₀ ≤ ValuationSpectrum.ringPlus A)
  (π : ↥P.A₀) (hI : P.I = Ideal.span {π})
  (hπ_tn :
    IsTopologicallyNilpotent
      (P.A₀.subtype π))
  (hπ_unit : IsUnit (P.A₀.subtype π))
  (hArch :
    ∀ (v : Spv A),
      MulArchimedean
        (ValuativeRel.ValueGroupWithZero
          A))
  (T : Finset A)
  (hT :
    ∀
      v ∈
        ValuationSpectrum.Spa A
          (ValuationSpectrum.ringPlus A),
      ∃ t ∈ T, ¬t ≤ᵥ 0) :
  ∃ s,
    ∀
      v ∈
        ValuationSpectrum.Spa A
          (ValuationSpectrum.ringPlus A),
      ∃ t ∈ T, ↑s ≤ᵥ t ∧ ¬t ≤ᵥ ↑s

**Wedhorn Corollary 7.32 (Tate version).**

For a Tate ring `A` with the hypotheses ensuring quasi-compactness of
`Spa(A, A⁺)` — pair of definition `P` with `P.A₀ ⊆ A⁺`, principal ideal
`P.I = (π)` with `π` a topologically nilpotent unit of `A`, and
MulArchimedean value groups — and a finite family `T ⊆ A` with no common
zero on `Spa(A, A⁺)`, there exists a unit `s ∈ Aˣ` such that for every
`v ∈ Spa(A, A⁺)`, some `t ∈ T` satisfies `v(s) < v(t)`.

Concretely, `s = π^(N+1)` for `N` extracted from the finite subcover by
`exists_dominatedBy_cover`.

Proof for Theorem 6.7

uses 1

Each point v \in \mathrm{Spa} admits a power \varpi^{n_v} of the pseudo-uniformiser with v(\varpi^{n_v}) \le v(f_i) for all i on a neighbourhood, because \varpi is topologically nilpotent and the f_i are finitely many. The sets where a fixed power works are open and cover \mathrm{Spa}; quasi-compactness (Theorem 6.3) extracts a finite subcover, and taking the maximal exponent produces a single dominating unit. Following Wedhorn Corollary 7.32.