Continuity of a valuation on a Huber ring

On a Huber ring the neighbourhood filter of 0 has a concrete basis — the images of the powers Iⁿ of an ideal of definition (TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero). Continuity of a valuation, which is openness of the sets {a | v a < v b}, can therefore be tested against that basis instead of against the topology: v is continuous exactly when each of those sets swallows some Iⁿ.

That replaces a quantifier over open sets by one over a single natural number, and it is the form Wedhorn's §7.2 arguments actually use — his proof of Theorem 7.10 produces continuity by exhibiting, for a given γ, an n with v < γ on Iⁿ⁺¹.

The codomain is a monoid, so Valuation.ltAddSubgroup is unavailable

Mathlib's Valuation.ltAddSubgroup packages a sublevel set as an additive subgroup, but it is indexed by Γ₀ˣ and so forces a LinearOrderedCommGroupWithZero codomain. IsContinuous is stated over a LinearOrderedCommMonoidWithZero, matching Mathlib's Valuation, and this criterion is stated over one too — the strict triangle inequality needs no inverses. The subgroup used below is therefore TauCeti.Valuation.ltAddSubgroupOfNeZero, the analogue of Mathlib's construction at the weaker codomain, rather than Mathlib's own.

Main results

• TauCeti.Huber.PairOfDefinition.isContinuous_iff_forall_exists_idealImage_subset : the criterion, in both directions.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition and Definition 6.1, and §7.2.
• AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, projects/AdicSpaces/Adic spaces/SpvAITopology.lean, was consulted. It names pow_image_isOpen and isContinuous_of_ideal_pow_lt as consumers of exactly this criterion, which is what fixed its downstream-facing shape, but does not state the criterion itself and leaves the surrounding Wedhorn 7.10 sub-leaves incomplete.

theorem TauCeti.Huber.PairOfDefinition.isContinuous_iff_forall_exists_idealImage_subset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (P : PairOfDefinition A) (v : Valuation A Γ₀) : v.IsContinuous ↔ ∀ (b : A), v b ≠ 0 → ∃ (n : ℕ), ↑(P.idealImage n) ⊆ {a : A | v a < v b}

Continuity, tested against the ideal-of-definition basis. A valuation on a Huber ring is continuous exactly when every set {a | v a < v b} contains the image of some power Iⁿ of an ideal of definition.

The b with v b = 0 are excluded because {a | v a < 0} is empty, hence not a subgroup; Valuation.isContinuous_iff_forall_ne_zero shows they cost nothing.