A continuous archimedean valuation is bounded by one on the power-bounded elements

Wedhorn Proposition 7.41. If v is a continuous valuation whose value group is archimedean, and some topologically nilpotent b has v b ≠ 0, then v a ≤ 1 for every power-bounded a.

The two hypotheses on v are what Wedhorn's x ∈ Cont(A)ᵃ of height 1 supplies. The archimedean condition is imposed on the value group MonoidWithZeroHom.ValueGroup₀ v, not on the codomain, which is what Mathlib's Valuation.nonempty_rankOne_iff_mulArchimedean actually yields from height one; a caller who happens to have an archimedean codomain gets the instance by MulArchimedean.comap embedding.toMonoidHom embedding_strictMono. The archimedean step therefore runs in Γ_v and transports back along the strictly monotone embedding. Analyticity gives the topologically nilpotent b with v b ≠ 0, which is Wedhorn's Remark 7.40(1).

The argument is Wedhorn's. Suppose 1 < v a. Archimedeanness gives n with (v b)⁻¹ ≤ v a ^ n, hence 1 ≤ v (a ^ n * b). But a ^ n is power-bounded and b is topologically nilpotent, so a ^ n * b is topologically nilpotent, and continuity forces v (a ^ n * b) < 1. The two bounds are incompatible, so no such a exists.

Main results

• Valuation.IsContinuous.le_one_of_isPowerBounded: Proposition 7.41. Stated in the Valuation.IsContinuous namespace so it is reachable by dot notation on the continuity hypothesis, alongside Valuation.IsContinuous.lt_one_of_isTopologicallyNilpotent.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.41, whose proof this follows step by step, together with Remark 7.40(1) for the witness b and Proposition 1.14 for height one implying archimedean.

theorem Valuation.IsContinuous.le_one_of_isPowerBounded {A : Type u_1} [CommRing A] [TopologicalSpace A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation A Γ₀} [MulArchimedean (↑v).ValueGroup₀] (hv : v.IsContinuous) {b : A} (hb : IsTopologicallyNilpotent b) (hb0 : v b ≠ 0) {a : A} (ha : TauCeti.Huber.IsPowerBounded a) : v a ≤ 1

Wedhorn Proposition 7.41. A continuous valuation whose value group is archimedean, and which is nonzero on some topologically nilpotent element, is bounded by 1 on the power-bounded elements.

The archimedean hypothesis is on the value group, which is what height one supplies; an archimedean codomain gives it by MulArchimedean.comap.

The witness b is what analyticity supplies (Wedhorn Remark 7.40(1)), and it is not removable. Give a reduced A the discrete topology: every element is then power-bounded, every valuation is continuous (Valuation.isContinuous_of_discreteTopology), and a power of x vanishes only if x does, so 0 is the sole topologically nilpotent element and no witness exists. Discrete ℚ carrying a p-adic valuation is such an A, and there 1 < v p⁻¹ refutes the conclusion.