Stable uniformity and the structure presheaf

Buzzard and Verberkmoes call a Tate pair (A, A⁺) stably uniform when 𝒪_X(U) is uniform for every rational subset U of X = Spa(A, A⁺). This file identifies that condition, for the presentation-indexed limit presentationLimit, with TauCeti.Huber.IsStablyUniform, the uniformity of every rational localization A⟨T/s⟩. It deduces that stable uniformity passes to rational localizations.

Main results

• TauCeti.Huber.isStablyUniform_iff_forall_isUniform_presentationLimit: for a subring A⁺ of power-bounded elements, A is stably uniform exactly when presentationLimit A⁺ V is uniform for every rational open V of Spa(A, A⁺).
• TauCeti.Huber.PairOfDefinition.isStablyUniform_completion_locTopology: a rational localization A⟨T/s⟩ of a stably uniform Tate ring is stably uniform.

References

• K. Buzzard, A. Verberkmoes, Stably uniform affinoids are sheafy, J. reine angew. Math. 740 (2018), 25–39, §3 and the proof of Theorem 7.
• D. Hansen, K. S. Kedlaya, Sheafiness criteria for Huber rings, Definition 3.13.
• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 8.2 (2) and Remark 8.4.

theorem TauCeti.Huber.isStablyUniform_iff_forall_isUniform_presentationLimit {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] (P : PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → IsPowerBounded a) : IsStablyUniform A ↔ ∀ V ∈ ValuationSpectrum.spaRationalOpens Aplus, IsUniform (ValuationSpectrum.presentationLimit Aplus V).obj.α

Stable uniformity of a pair. Let P be a pair of definition of A and A⁺ a subring of power-bounded elements. Then A is stably uniform exactly when presentationLimit A⁺ V is uniform for every rational open V of Spa(A, A⁺); on V = R(T/s) this limit is A⟨T/s⟩ by presentationLimitRationalIso. The left side involves neither P nor A⁺, so the right side holds for one such choice exactly when it holds for all of them. Unlike isStablyUniform_iff_forall_isUniform_completionLocObj, which ranges over presentations (T, s), this ranges over the rational opens themselves.

theorem TauCeti.Huber.PairOfDefinition.isStablyUniform_completion_locTopology {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsStablyUniform A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hT : IsOpen ↑(Ideal.span ↑T)) : IsStablyUniform (UniformSpace.Completion S)

A rational localization of a stably uniform Tate ring is stably uniform (Buzzard and Verberkmoes, proof of Theorem 7): if T spans an open ideal of A, then A⟨T/s⟩ is stably uniform when A is. Here A⟨T/s⟩ is UniformSpace.Completion S for the uniformity locUniformSpace P T s S hden, a Tate ring by isTateRing_completion_locTopology_of_isTateRing. For hden one may take hasDenominatorPower_of_isOpen_span P T s S hT.