Uniform Huber rings

A topological ring A is uniform when its set A° of power-bounded elements is bounded (Hansen–Kedlaya, Definition 2.3). Uniformity is the hypothesis of the Buzzard–Verberkmoes sheafiness criterion: if every rational localisation of a complete Tate ring is uniform, then the structure presheaf of its adic spectrum is a sheaf, with no noetherian hypothesis.

For a Huber ring, A° is always an open subring, so by Wedhorn's Lemma 6.2 uniformity says exactly that A° is itself a ring of definition. In a uniform Tate ring every nilpotent element lies in the closure of zero, so a Hausdorff uniform Tate ring is reduced: a Hausdorff Tate ring with a nonzero nilpotent element is not uniform.

Main definitions

• TauCeti.Huber.IsUniform: the power-bounded elements form a bounded set.

Main results

• TauCeti.Huber.isUniform_iff_exists_pairOfDefinition_ringOfDefinition_eq: a Huber ring is uniform exactly when A° is a ring of definition.
• TauCeti.Huber.isUniform_iff_of_ringEquiv: uniformity transports along topological ring isomorphisms; CategoryTheory.Iso.isUniform_iff is the same statement for isomorphisms in TopCommRingCat.
• TauCeti.Huber.IsUniform.nilradical_le_closure_bot: in a uniform Tate ring every nilpotent element lies in the closure of zero.
• TauCeti.Huber.IsUniform.isReduced: a Hausdorff uniform Tate ring is reduced.

Discrete rings are uniform (TauCeti.Huber.IsUniform.of_discreteTopology), and so are normed division rings, by TauCeti.Huber.IsUniform.of_normedDivisionRing in TauCeti.RingTheory.Huber.Normed.

References

• D. Hansen, K. S. Kedlaya, Sheafiness criteria for Huber rings, Definition 2.3.
• K. Buzzard, A. Verberkmoes, Stably uniform affinoids are sheafy, J. reine angew. Math. 740 (2018).
• Wedhorn, Adic Spaces, Lemma 6.2 and Corollary 6.4.

class TauCeti.Huber.IsUniform (A : Type u_1) [MonoidWithZero A] [TopologicalSpace A] : Prop

A topological ring is uniform when its power-bounded elements form a bounded set (Hansen–Kedlaya, Definition 2.3).

• isBounded_setOf_isPowerBounded : IsBounded {a : A | IsPowerBounded a}

  The set A° of power-bounded elements is bounded.

theorem TauCeti.Huber.isUniform_iff {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] : IsUniform A ↔ IsBounded {a : A | IsPowerBounded a}

Unfolding lemma for TauCeti.Huber.IsUniform.

@[instance 100]

instance TauCeti.Huber.IsUniform.of_discreteTopology {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] [DiscreteTopology A] : IsUniform A

Discrete rings are uniform: in the discrete topology every set is bounded.

theorem TauCeti.Huber.isUniform_iff_of_ringEquiv {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsUniform A ↔ IsUniform B

Uniformity transports along a topological ring isomorphism.

theorem TauCeti.Huber.IsUniform.of_ringEquiv {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] [IsUniform A] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsUniform B

A topological ring isomorphic to a uniform one is uniform.

theorem TauCeti.Huber.isUniform_iff_isBounded_powerBoundedSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : IsUniform A ↔ IsBounded ↑(powerBoundedSubring A)

A nonarchimedean ring is uniform exactly when its power-bounded subring A° is bounded.

theorem TauCeti.Huber.IsUniform.isBounded_powerBoundedSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [IsUniform A] : IsBounded ↑(powerBoundedSubring A)

In a uniform nonarchimedean ring the power-bounded subring A° is bounded.

theorem TauCeti.Huber.isUniform_iff_exists_pairOfDefinition_ringOfDefinition_eq {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] : IsUniform A ↔ ∃ (Q : PairOfDefinition A), Q.ringOfDefinition = powerBoundedSubring A

A Huber ring is uniform exactly when A° is a ring of definition, that is, when some pair of definition has A° as its ring.

theorem TauCeti.Huber.IsUniform.nilradical_le_closure_bot_of_isPseudoUniformizer {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsUniform A] {ϖ : A} (hϖ : IsPseudoUniformizer ϖ) : nilradical A ≤ ⊥.closure

In a uniform topological ring with a pseudo-uniformizer, every nilpotent element lies in the closure of zero.

theorem TauCeti.Huber.IsUniform.isReduced_of_isPseudoUniformizer {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsUniform A] [T0Space A] {ϖ : A} (hϖ : IsPseudoUniformizer ϖ) : IsReduced A

A Hausdorff uniform topological ring with a pseudo-uniformizer is reduced.

theorem TauCeti.Huber.IsUniform.nilradical_le_closure_bot {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsUniform A] : nilradical A ≤ ⊥.closure

In a uniform Tate ring every nilpotent element lies in the closure of zero.

theorem TauCeti.Huber.IsUniform.isReduced {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] [IsUniform A] [T0Space A] : IsReduced A

A Hausdorff uniform Tate ring is reduced.

theorem CategoryTheory.Iso.isUniform_iff {R S : TopCommRingCat} (e : R ≅ S) : TauCeti.Huber.IsUniform R.α ↔ TauCeti.Huber.IsUniform S.α

Uniformity is invariant under isomorphism in TopCommRingCat. For an isomorphism e in the full subcategory of an object property P, apply this to P.ι.mapIso e, its image under the inclusion. The unbundled form, for a ring isomorphism continuous in both directions, is TauCeti.Huber.isUniform_iff_of_ringEquiv.