Emptiness of the analytic locus

This file completes Wedhorn's criterion for the analytic locus of a Huber pair to be empty. For a pair of definition (A₀, I), the difficult implication starts with two prime ideals p ⊆ q of A₀, where q contains I. If p did not contain I, a valuation ring of the residue field at p dominating the image of q would give a valuation with support p and value < 1 on q. Restricting its value group to the convex subgroup generated by one maximal nonzero value on a finite generating set of I, then extending from A₀ to A, produces a continuous analytic point. Thus emptiness forces I ⊆ p.

After localising A₀ at 1 + I, every prime contracts to such a p and admits a specialisation containing I. Hence the image of I lies in every prime of the localisation. The ideal-theoretic result Ideal.exists_forall_pow_eq_pow makes the powers of I eventually constant. Their images are a neighbourhood basis of zero in A, so the closure of zero is open and the separated quotient is discrete.

Main result

• TauCeti.ValuationSpectrum.spaAnalytic_eq_empty_iff_discrete_separationQuotient: Wedhorn Proposition 7.49(2), the analytic locus is empty exactly when the separated quotient is discrete.

References

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

theorem TauCeti.ValuationSpectrum.spaAnalytic_eq_empty_iff_discrete_separationQuotient {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) (hAplus : Aplus ≤ Huber.powerBoundedSubring A) : spaAnalytic Aplus = ∅ ↔ DiscreteTopology (SeparationQuotient A)

Wedhorn Proposition 7.49(2). If Aplus consists of power-bounded elements (in particular, if it is a ring of integral elements), its analytic locus is empty if and only if the separated quotient of the Huber ring A is discrete.