5. Integral elements and affinoid rings🔗

Definition5.1

Statement uses 2

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 5.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For a topological ring A, a subring A^{+} \subseteq A is a ring of integral elements (\texttt{IsRingOfIntegralElements}) if it is open, integrally closed in A, and contained in the power-bounded subring A^{\circ} (Definition 1.1, Definition 2.1). The pair (A, A^{+}) is then an affinoid ring (Huber pair), \texttt{IsAffinoidRing}. Following Wedhorn Definition 7.14.

Lean code for Definition5.1●2 definitions

class(3 methods)defined in «Adic spaces»/AffinoidRings.lean

complete

class ValuationSpectrum.IsRingOfIntegralElements.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] (B : Subring A) : Prop

class ValuationSpectrum.IsRingOfIntegralElements.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A] (B : Subring A) :
  Prop

A ring of integral elements (Definition 7.14(1)): open, integrally closed, and in `A°`.

A `class` (not a bare `structure`) so it can be required as `[IsRingOfIntegralElements (A⁺)]`
on `Spa`-level theorems — the faithful affinoid-ring interface (expert-review 2026-06-18,
reviewer Q1). The bare `PlusSubring` carrier stays low-level; this records the three
Definition-7.14 axioms (open, integrally closed, `⊆ A°`) that make `(A, A⁺)` an affinoid ring.

Methods

isOpen : IsOpen ↑B

`B` is open in `A`.

isIntegrallyClosed : ∀ (a : A), IsIntegral (↥B) a → a ∈ B

`B` is integrally closed in `A`.

subset_powerBounded : ↑B ⊆ TopologicalRing.powerBoundedSubring A

`B ⊆ A°`.

defdefined in «Adic spaces»/AffinoidRings.lean

complete

def ValuationSpectrum.IsAffinoidRing.{u_2} (A : Type u_2) [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] : Prop

def ValuationSpectrum.IsAffinoidRing.{u_2}
  (A : Type u_2) [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A] : Prop

`(A, A⁺)` is an affinoid ring if `A⁺` is a ring of integral elements (Definition 7.14).

Theorem5.2

Statement uses 2

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Every ring of integral elements A^{+} is contained in A^{\circ} and contains all topologically nilpotent elements: A^{\circ\circ} \subseteq A^{+} \subseteq A^{\circ} (Definition 5.1, Definition 2.1). Following Wedhorn Remark 7.15.

Lean code for Theorem5.2●2 theorems

theoremdefined in «Adic spaces»/AffinoidRings.lean

complete

theorem ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring.{u_1}
  {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Subring A}
  (hB : ValuationSpectrum.IsRingOfIntegralElements B) :
  ↑B ⊆ TopologicalRing.powerBoundedSubring A

theorem ValuationSpectrum.IsRingOfIntegralElements.le_powerBoundedSubring.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A] {B : Subring A}
  (hB :
    ValuationSpectrum.IsRingOfIntegralElements
      B) :
  ↑B ⊆
    TopologicalRing.powerBoundedSubring A

Any ring of integral elements is contained in `A°` (Remark 7.15(1)).

theoremdefined in «Adic spaces»/AffinoidRings.lean

complete

theorem ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset.{u_1}
  {A : Type u_1} [CommRing A] [TopologicalSpace A] {B : Subring A}
  (hB : ValuationSpectrum.IsRingOfIntegralElements B) :
  TopologicalRing.topologicallyNilpotentElements A ⊆ ↑B

theorem ValuationSpectrum.IsRingOfIntegralElements.topologicallyNilpotentElements_subset.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A] {B : Subring A}
  (hB :
    ValuationSpectrum.IsRingOfIntegralElements
      B) :
  TopologicalRing.topologicallyNilpotentElements
      A ⊆
    ↑B

A ring of integral elements contains all topologically nilpotent elements.

Proof for Theorem 5.2

uses 0

By definition A^{+} \subseteq A^{\circ}. Conversely a topologically nilpotent element t satisfies t^n \to 0, so 1 - t is a unit and t is integral over A^{+} after clearing by an open neighbourhood; openness and integral-closedness of A^{+} then force t \in A^{+}. Hence A^{\circ\circ} \subseteq A^{+}. Following Wedhorn Remark 7.15.

Definition5.3

Statement uses 2

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

A Huber ring A is uniform if A^{\circ} is bounded (\texttt{IsUniform}); an affinoid ring (A, A^{+}) is stably uniform if every rational localisation stays uniform (\texttt{IsStablyUniform}) (Definition 5.1, Definition 2.1). Stable uniformity is the standard hypothesis guaranteeing the structure presheaf is a sheaf. Following Wedhorn Definitions 7.36 and 7.37.

Lean code for Definition5.3●2 definitions

class(1 method)defined in «Adic spaces»/Uniform.lean

complete

class TopologicalRing.IsUniform.{u} (A : Type u) [CommRing A]
  [TopologicalSpace A] : Prop

class TopologicalRing.IsUniform.{u} (A : Type u)
  [CommRing A] [TopologicalSpace A] : Prop

A topological ring `A` is **uniform** if the set `A°` of power-bounded elements is
bounded (Definition 7.36 of Wedhorn).

Methods

isBounded_powerBounded : TopologicalRing.IsBounded (TopologicalRing.powerBoundedSubring A)

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

class(1 method)defined in «Adic spaces»/Uniform.lean

complete

class TopologicalRing.IsStablyUniform.{u} (A : Type u) [CommRing A]
  [TopologicalSpace A] [IsTopologicalRing A]
  [ValuationSpectrum.PlusSubring A] [IsHuberRing A] : Prop

class TopologicalRing.IsStablyUniform.{u}
  (A : Type u) [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  [ValuationSpectrum.PlusSubring A]
  [IsHuberRing A] : Prop

A Huber pair `(A, A⁺)` is **stably uniform** if for every rational localization
`(A, A⁺) → (B, B⁺)`, the localization ring `B` (with the localization topology) is
uniform (Definition 7.37 of Wedhorn).

Methods

presheafValue_isUniform : ∀ (D : ValuationSpectrum.RationalLocData A),
  TopologicalRing.IsBounded (TopologicalRing.powerBoundedSubring (ValuationSpectrum.presheafValue D))

The presheaf value (= completion of the localization) is uniform for every
rational localization datum `D`.