Cofinal values on a generating set make a valuation continuous

Wedhorn, Adic Spaces (arXiv:1910.05934v1), the engine of Theorem 7.10's ⊇ direction.

A valuation on a Huber ring is continuous as soon as it is bounded by 1 on an ideal of definition I and has cofinal values on a generating set of I. That is exactly what the right-hand side of Theorem 7.10 supplies: membership in Spv (A, IA) gives the cofinality through Wedhorn Lemma 7.4 — on its cofinal branch directly, and on its full-characteristic-group branch through cofinalValue_of_hasFullCharacteristicGroup below, since v a < 1 on I places the open ideal image, a neighbourhood of 0, inside the unit ball — so the unit ball is itself a neighbourhood of 0. The same v a < 1 gives the bound.

What the argument actually needs

Continuity is tested against the basic neighbourhoods Iⁿ of zero (TauCeti.Huber.PairOfDefinition.isContinuous_iff_forall_exists_idealImage_subset), so given b with v b ≠ 0 the task is to find one n with v < v b on the image of Iⁿ.

Only one generator has to be cofinal: one whose value dominates the others. Cofinality there produces an n with v t₀ ⁿ < v b, the valuation bound on a power of a spanned ideal (Valuation.map_le_pow_of_mem_span_pow_succ) gives v ≤ v t₀ ⁿ on Iⁿ⁺¹, and the two inequalities compose. That is isContinuous_of_forall_le_of_cofinalValue, which asks for no finiteness at all.

The form a call site actually holds — a finite generating set with every generator cofinal, as Lemma 7.4 hands over — is the corollary isContinuous_of_forall_cofinalValue. Finiteness enters there and only there, to produce the dominating generator as a maximum.

Why the bound is taken over A₀

The valuation bound is applied through v.comap P.ringOfDefinition.subtype, over the ring of definition rather than over A. That is forced rather than cosmetic. An element of Iⁿ⁺¹ is a sum of terms c * t₀ * ⋯ * tₙ whose coefficient c ranges over A₀, so the coefficient can be absorbed into a generator — c * t₀ lies in I, where v ≤ 1 is available. Over the extension I · A the coefficients range over all of A instead, and v ≤ 1 on I · A does not follow from these hypotheses.

Main results

• TauCeti.Huber.PairOfDefinition.isContinuous_of_forall_le_of_cofinalValue : the engine, needing cofinality at a single dominating generator.
• TauCeti.Huber.PairOfDefinition.isContinuous_of_forall_cofinalValue : its call-site form, for a finite generating set with every generator cofinal.
• TauCeti.Huber.PairOfDefinition.cofinalValue_of_hasFullCharacteristicGroup : the supply for Lemma 7.4's other branch — a full characteristic group makes every ideal-of-definition value cofinal, given v a < 1 on the ideal of definition.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Theorem 7.10 and Lemma 7.4.

theorem TauCeti.Huber.PairOfDefinition.isContinuous_of_forall_le_of_cofinalValue {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (P : PairOfDefinition A) (v : Valuation A Γ₀) {s : Set ↥P.ringOfDefinition} {t₀ : ↥P.ringOfDefinition} (hgen : Ideal.span s = P.idealOfDefinition) (hle : ∀ t ∈ s, v ↑t ≤ v ↑t₀) (h1 : ∀ a ∈ P.idealOfDefinition, v ↑a ≤ 1) (hcof : v.CofinalValue ↑t₀) : v.IsContinuous

A single dominating cofinal generator makes a valuation continuous. If v ≤ 1 on an ideal of definition I, and I is spanned by a set whose values v bounds by that of some t₀ with cofinal value, then v is continuous.

No finiteness is needed: the spanning set is an arbitrary Set, cofinality is asked of t₀ alone, and t₀ need not even lie in the spanning set — dominating it is enough. isContinuous_of_forall_cofinalValue below is the reading a call site usually holds.

theorem TauCeti.Huber.PairOfDefinition.isContinuous_of_forall_cofinalValue {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (P : PairOfDefinition A) (v : Valuation A Γ₀) {s : Finset ↥P.ringOfDefinition} (hgen : Ideal.span ↑s = P.idealOfDefinition) (h1 : ∀ a ∈ P.idealOfDefinition, v ↑a ≤ 1) (hcof : ∀ t ∈ s, v.CofinalValue ↑t) : v.IsContinuous

Cofinal values on a finite generating set make a valuation continuous. If v ≤ 1 on an ideal of definition I and v has cofinal values at every member of a finite generating set of I, then v is continuous.

This is the engine above with the dominating generator produced as a maximum, which is the only thing finiteness is used for. The empty generating set is allowed: it forces I = ⊥, whose first basic neighbourhood is already {0}.

It is the form Wedhorn Theorem 7.10's ⊇ direction hands over: membership in Spv (A, IA) supplies the cofinality through Lemma 7.4, and v a < 1 on I supplies the bound.

theorem TauCeti.Huber.PairOfDefinition.cofinalValue_of_hasFullCharacteristicGroup {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (P : PairOfDefinition A) (v : Valuation A Γ₀) (hfull : v.HasFullCharacteristicGroup) (h1 : ∀ a ∈ P.idealOfDefinition, v ↑a < 1) {x : ↥P.ringOfDefinition} (hx : x ∈ P.idealOfDefinition) : v.CofinalValue ↑x

Full characteristic group makes every ideal-of-definition value cofinal, given the sub-unit bound v a < 1 on the ideal of definition.

This is the Γ_v = cΓ_v branch of Wedhorn's proof of Theorem 7.10, ⊇ direction: Lemma 7.4 splits membership in Spv (A, IA) into cofinality on IA — which isContinuous_of_forall_cofinalValue consumes directly — or full characteristic group, which this lemma reduces to the first case. The sub-unit bound is what hands the valuation-level lemma its neighbourhood: v a < 1 on I places the open ideal image inside the unit ball, so the unit ball is itself a neighbourhood of 0.