The adic spectrum of a normed field

For a normed field K with an ultrametric norm, every point v of Spa (K, K°) compares elements of K exactly as the norm does: v(x) ≤ v(y) if and only if ‖x‖ ≤ ‖y‖. The plus ring K° is the closed unit ball, which gives one direction, and continuity of v gives the other, since an element of norm less than one is topologically nilpotent.

This is how points of Spa (K, K°) enter computations on spaces over K: whenever a point of an adic spectrum over K pulls back to Spa (K, K°), as every point of the closed polydisc does along the constant embedding, it compares constants by their norms.

Main results

• TauCeti.ValuationSpectrum.vle_iff_norm_le_of_mem_spa: every point of Spa (K, K°) compares elements of K by their norms.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.23 and Example 7.57.

theorem TauCeti.ValuationSpectrum.vle_iff_norm_le_of_mem_spa {K : Type u_1} [NormedField K] [IsUltrametricDist K] {v : ValuationSpectrum K} (hv : v ∈ spa (Huber.powerBoundedSubring K)) (x y : K) : x ≤ᵥ y ↔ ‖x‖ ≤ ‖y‖

Every point of Spa (K, K°) compares elements of K by their norms. If ‖x‖ ≤ ‖y‖ then x / y is power-bounded, so v(x / y) ≤ 1. If ‖y‖ < ‖x‖ then y / x is topologically nilpotent, so v(y / x) < 1 by continuity.