Rational subsets do not move under small perturbations

A strengthening of Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.34. Wedhorn assumes a complete Hausdorff affinoid ring; the results here need only a Huber ring A. Fix a pair of definition (A₀, I), a ring of integral elements A⁺, a finite numerator set T whose ideal T · A is open, and a denominator s. There is a basic neighbourhood Iⁿ of zero such that replacing each numerator and the denominator by anything within Iⁿ of it leaves the rational subset unchanged:

R(T'/s') = R(T/s).

The perturbed data are not indexed by T: T' is any finite set each of whose elements is Iⁿ-close to some element of T and which has an Iⁿ-close element for each of them. That is what the statement actually needs, and it avoids carrying a bijection T ≃ T' — the same set may be presented with different cardinality after perturbation.

The same estimate settles a second way of leaving a rational subset where it is: enlarging the numerator set by elements too small to matter. Along a continuous homomorphism φ : A → B of Huber rings, a rational subset R(T/s) of Spa(B, B⁺) with T · B open admits a finite D ⊆ A spanning an open ideal of A whose image may be adjoined to T for free.

Main results

• TauCeti.ValuationSpectrum.valuation_lt_of_mem_idealImage : elements of a sufficiently small basic neighbourhood have value strictly below the rational subset's denominator.
• TauCeti.ValuationSpectrum.exists_forall_rationalSubset_eq_of_sub_mem_idealImage : Proposition 7.34, with the perturbation measured by an explicit power of the ideal of definition.
• TauCeti.ValuationSpectrum.exists_mem_nhds_forall_rationalSubset_eq_of_sub_mem : the same statement over a Huber ring, with the perturbation measured by a neighbourhood of zero and no pair of definition in sight.
• TauCeti.ValuationSpectrum.exists_isOpen_span_rationalSubset_union_image_eq : a rational subset is unchanged by adjoining the image of a suitable finite set spanning an open ideal of the source of a continuous homomorphism.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.29, Proposition 7.34, and the enlargement of a numerator set carried out in the proof of Proposition 8.2(2).

theorem TauCeti.ValuationSpectrum.valuation_lt_of_mem_idealImage {A : Type u_1} [CommRing A] [TopologicalSpace A] (P : Huber.PairOfDefinition A) {T : Finset A} {n : ℕ} (hdec : ∀ a ∈ P.idealImage n, ∃ (w : A → A), (∀ t ∈ T, w t ∈ P.idealImage 1) ∧ ∑ t ∈ T, t * w t = a) {v : ValuationSpectrum A} (hv : v.IsContinuous) {s : A} (hs : v.valuation s ≠ 0) (hle : ∀ t ∈ T, v.valuation t ≤ v.valuation s) {a : A} (ha : a ∈ P.idealImage n) : v.valuation a < v.valuation s

A neighbourhood of zero is strictly dominated by the denominator of a rational subset. If the numerator ideal T · A supplies the decomposition of TauCeti.Huber.PairOfDefinition.exists_forall_mem_idealImage_exists_sum_eq in degree n, then at a continuous point at which every t ∈ T is dominated by a nonzero v s, every element of Iⁿ has value strictly below v s.

The hypothesis is the decomposition itself rather than the openness of T · A, because TauCeti.ValuationSpectrum.exists_forall_rationalSubset_eq_of_sub_mem_idealImage applies the estimate with two different denominators and one fixed exponent.

theorem TauCeti.ValuationSpectrum.exists_forall_rationalSubset_eq_of_sub_mem_idealImage {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (hT : IsOpen ↑(Ideal.span ↑T)) (s : A) : ∃ (n : ℕ), ∀ (T' : Finset A) (s' : A), (∀ t ∈ T, ∃ u ∈ T', t - u ∈ P.idealImage n) → (∀ u ∈ T', ∃ t ∈ T, u - t ∈ P.idealImage n) → s - s' ∈ P.idealImage n → rationalSubset Aplus T' s' = rationalSubset Aplus T s

A strengthening of Wedhorn Proposition 7.34. Wedhorn assumes a complete Hausdorff affinoid ring; here, for a numerator set T in a Huber ring with T · A open, there is an exponent n such that perturbing the numerators and the denominator inside the basic neighbourhood Iⁿ of zero does not change the rational subset.

The two matching hypotheses say that T' and T are Iⁿ-close as sets: every perturbed numerator is near an original one and conversely. No hypothesis is placed on T' · A, and A is not assumed complete.

theorem TauCeti.ValuationSpectrum.exists_mem_nhds_forall_rationalSubset_eq_of_sub_mem {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) (T : Finset A) (hT : IsOpen ↑(Ideal.span ↑T)) (s : A) : ∃ V ∈ nhds 0, ∀ (T' : Finset A) (s' : A), (∀ t ∈ T, ∃ u ∈ T', t - u ∈ V) → (∀ u ∈ T', ∃ t ∈ T, u - t ∈ V) → s - s' ∈ V → rationalSubset Aplus T' s' = rationalSubset Aplus T s

A generalization of Wedhorn Proposition 7.34. The source assumes a complete Hausdorff affinoid ring; this theorem shows that, already over a Huber ring, a rational subset with open numerator ideal is unchanged by perturbing its defining data inside a suitable neighbourhood of zero.

This is the form the later theory uses: no pair of definition appears, so the neighbourhood is the only datum a caller has to produce.

theorem TauCeti.ValuationSpectrum.exists_isOpen_span_rationalSubset_union_image_eq {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] {B : Type u_2} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [Huber.IsHuberRing B] {φ : A →+* B} (hφ : Continuous ⇑φ) (Bplus : Subring B) (T : Finset B) (hT : IsOpen ↑(Ideal.span ↑T)) (s : B) : ∃ (D : Finset A), IsOpen ↑(Ideal.span ↑D) ∧ rationalSubset Bplus (T ∪ Finset.image (⇑φ) D) s = rationalSubset Bplus T s

A rational subset absorbs the image of a small enough open-spanning finite set. Along a continuous homomorphism φ : A → B of Huber rings, a rational subset R(T/s) of Spa(B, B⁺) whose numerator ideal T · B is open admits a finite D ⊆ A spanning an open ideal of A whose image may be adjoined to the numerators for free:

R((T ∪ φ(D))/s) = R(T/s).

Wedhorn carries out this enlargement inside the proof of Proposition 8.2(2). Neither ring is assumed Tate, complete or Noetherian, and nothing is assumed relating the ideals of definition of A and B: the ideal D · A is open for reasons internal to A.