Continuity of real valuations on adic rings #
Let A be a ring whose topology is the I-adic one, for an ideal I = Ideal.span s. A valuation
v : Valuation A ℝ≥0 that is at most 1 on I and at most some c < 1 on the generators s is
continuous: by Valuation.map_le_pow_of_mem_span_pow_succ it is at most c ^ N on I ^ (N + 1),
and these open ideals form a basis of neighbourhoods of 0. This is how rank-one points of adic
spectra, such as the Gauss points of Spa(A_inf, A_inf), are shown to be continuous.
Main results #
Valuation.isContinuous_of_isAdic: the continuity criterion.
theorem
Valuation.isContinuous_of_isAdic
{A : Type u_1}
[CommRing A]
[TopologicalSpace A]
{v : Valuation A NNReal}
{s : Set A}
{c : NNReal}
(hI : IsAdic (Ideal.span s))
(h1 : ∀ a ∈ Ideal.span s, v a ≤ 1)
(hc : c < 1)
(hs : ∀ t ∈ s, v t ≤ c)
:
Continuity of real valuations on adic rings. If the topology of A is the I-adic one
for I = Ideal.span s, a valuation v : Valuation A ℝ≥0 that is at most 1 on I and at most
some c < 1 on s is continuous.