Documentation

TauCeti.RingTheory.Huber.StableUniform

Stably uniform Tate rings #

A Tate ring is stably uniform when each of its completed rational localizations is uniform. A rational localization is represented by a finite numerator set T, a denominator s, and the condition that the ideal spanned by T is open. The coordinate ring is the separated completion A⟨T/s⟩ of the corresponding topological localization. This is Wedhorn's convention; a presentation in the convention where only insert s T must generate the unit ideal is covered by the numerator set insert s T, which has the same ring A₀[T/s] by TauCeti.Huber.PairOfDefinition.locSubring_insert_eq_of_divBy_mem (as s/s = 1).

The definition quantifies over pairs of definition because the current construction of A⟨T/s⟩ uses one to present its topology. The ring A⟨T/s⟩ does not depend on that choice (TauCeti.Huber.PairOfDefinition.completionLocObj_congr_pairOfDefinition), so the rational localizations over a single pair of definition already decide stable uniformity. The definition does not involve a ring of integral elements: stable uniformity is a property of the underlying Tate ring, not of the choice of plus ring.

The definition needs no completeness or separation hypothesis on A, since each A⟨T/s⟩ is itself a separated completion. When A is complete and Hausdorff, the trivial rational localization A⟨{1}/1⟩ is canonically isomorphic to A. Consequently, stable uniformity then implies uniformity of A itself; this is the first basic consequence needed by the Buzzard–Verberkmoes sheafiness criterion.

Main definitions #

Main results #

References #

source
class TauCeti.Huber.IsStablyUniform (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] :
Prop

A Tate ring is stably uniform when every completed rational localization A⟨T/s⟩ is uniform. The openness of the ideal spanned by T is exactly the admissibility condition for the rational localization; it supplies the denominator-power hypothesis needed to construct its topology.

Instances
    source
    theorem TauCeti.Huber.isStablyUniform_iff (A : Type u_1) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] :
    IsStablyUniform A ↔ ∀ (P : PairOfDefinition A) (T : Finset A) (s : A) (hT : IsOpen ↑(Ideal.span ↑T)), have hden := ⋯; IsUniform (UniformSpace.Completion (Localization.Away s))

    The defining property of stable uniformity: all admissible completed rational localizations are uniform.

    source
    theorem TauCeti.Huber.isStablyUniform_iff_forall_isUniform_completionLocObj {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] (P : PairOfDefinition A) :
    IsStablyUniform A ↔ ∀ (T : Finset A) (s : A) (hT : IsOpen ↑(Ideal.span ↑T)), IsUniform (P.completionLocObj T s (Localization.Away s) ⋯).obj.α

    One pair of definition suffices: for any fixed pair of definition P, a Tate ring is stably uniform exactly when its admissible completed rational localizations A⟨T/s⟩ over P are uniform. Unlike isStablyUniform_iff, which ranges over all pairs of definition, the localizations here are the bundled objects P.completionLocObj of CompleteSeparatedTopCommRingCat, so uniformity can be moved along isomorphisms of these objects with CategoryTheory.Iso.isUniform_iff.

    source
    theorem TauCeti.Huber.IsStablyUniform.isUniform {A : Type u_2} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [IsTateRing A] [IsStablyUniform A] :
    IsUniform A

    A stably uniform complete Hausdorff Tate ring is uniform. This is stable uniformity applied to the trivial rational localization A⟨{1}/1⟩, transported back along its canonical topological ring isomorphism with A.