Emptiness of the adic spectrum

For a Huber pair (A, A⁺), Wedhorn Proposition 7.49(1) characterizes emptiness of the adic spectrum by triviality of the separated quotient:

Spa(A, A⁺) = ∅  ↔  A / closure {0} = 0.

Since closure {0} is the kernel of the map to the separated quotient, this is equivalent to saying that the spectrum is empty exactly when 1 lies in closure {0}, that is, when 0 and 1 are topologically indistinguishable. So a Huber pair carries a continuous valuation unless its separated quotient is the zero ring.

For a Hausdorff Huber ring the closure of zero is {0}, giving the familiar criterion that the adic spectrum is empty exactly when the ring is trivial. In this form the criteria are the usual way to produce a point of Spa(A, A⁺), hence a continuous valuation on A.

Main results

• TauCeti.ValuationSpectrum.spa_eq_empty_iff_one_mem_closure_zero: the closure-of-zero form.
• TauCeti.ValuationSpectrum.spa_eq_empty_iff_subsingleton_quotient_closure_zero: the separated quotient form.
• TauCeti.ValuationSpectrum.spa_eq_empty_iff_subsingleton: the Hausdorff specialization.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.49(1).

Provenance

Developed here; nothing is ported. No external formalization is followed.

theorem TauCeti.ValuationSpectrum.one_mem_closure_zero_of_spa_eq_empty {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (hspa : spa Aplus = ∅) : 1 ∈ closure {0}

The converse half of Wedhorn Proposition 7.49(1). If the adic spectrum of a Huber pair (A, A⁺) is empty, then 1 belongs to the closure of zero, so 0 and 1 are topologically indistinguishable in A.

Emptiness is genuinely a Huber-pair phenomenon: hplus says A⁺ is a ring of integral elements, and without it a topological ring with no continuous valuation need not have 1 ∈ closure {0}.

theorem TauCeti.ValuationSpectrum.spa_eq_empty_iff_one_mem_closure_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) : spa Aplus = ∅ ↔ 1 ∈ closure {0}

Wedhorn Proposition 7.49(1), closure form. The adic spectrum of a Huber pair is empty exactly when 1 belongs to the closure of zero.

theorem TauCeti.ValuationSpectrum.spa_eq_empty_iff_subsingleton_quotient_closure_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) : spa Aplus = ∅ ↔ Subsingleton (A ⧸ ⊥.closure)

Wedhorn Proposition 7.49(1), separated-quotient form. The adic spectrum of a Huber pair is empty exactly when the quotient by the closure of zero is the zero ring.

theorem TauCeti.ValuationSpectrum.spa_eq_empty_iff_subsingleton {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] [T2Space A] (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) : spa Aplus = ∅ ↔ Subsingleton A

For a Hausdorff Huber pair, the adic spectrum is empty exactly when the underlying ring is trivial.