Adic Spaces — Lean blueprint

2. Bounded sets, power-bounded elements and open ideals🔗

Definition2.1
uses 0
Used by 6
Reverse dependency previews
Preview
Theorem 2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A subset S of a topological ring is bounded if it is absorbed by every neighbourhood of 0; an element a is power-bounded when \{a^n\} is bounded, and topologically nilpotent when a^n \to 0. The power-bounded elements form the subset A^{\circ} (\texttt{powerBoundedSubring}) and the topologically nilpotent ones the subset A^{\circ\circ} (\texttt{topologicallyNilpotentElements}). Following Wedhorn Definition 5.27.

Lean code for Definition2.1●2 definitions
  • defdefined in «Adic spaces»/Bounded.lean
    complete
    def TopologicalRing.powerBoundedSubring.{u_2} (A : Type u_2) [CommRing A]
  [TopologicalSpace A] : Set A
    def TopologicalRing.powerBoundedSubring.{u_2}
  (A : Type u_2) [CommRing A]
  [TopologicalSpace A] : Set A
    The set `A°` of all power-bounded elements.
  • defdefined in «Adic spaces»/Bounded.lean
    complete
    def TopologicalRing.topologicallyNilpotentElements.{u_2} (A : Type u_2)
  [CommRing A] [TopologicalSpace A] : Set A
    def TopologicalRing.topologicallyNilpotentElements.{u_2}
  (A : Type u_2) [CommRing A]
  [TopologicalSpace A] : Set A
    The set `A°°` of all topologically nilpotent elements (Definition 5.25).
Theorem2.2
uses 1used by 0✓L∃∀N

In a non-archimedean ring the sum of two power-bounded elements is again power-bounded; consequently A^{\circ} is a subring (Definition 2.1). Following Wedhorn Proposition 5.30(3).

Lean code for Theorem2.2●1 theorem
  • theoremdefined in «Adic spaces»/Bounded.lean
    complete
    theorem TopologicalRing.isPowerBounded_add.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [IsTopologicalRing A] [NonarchimedeanAddGroup A]
  {a b : A} (ha : TopologicalRing.IsPowerBounded a)
  (hb : TopologicalRing.IsPowerBounded b) :
  TopologicalRing.IsPowerBounded (a + b)
    theorem TopologicalRing.isPowerBounded_add.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  [NonarchimedeanAddGroup A] {a b : A}
  (ha : TopologicalRing.IsPowerBounded a)
  (hb :
    TopologicalRing.IsPowerBounded b) :
  TopologicalRing.IsPowerBounded (a + b)
    Sum of two power-bounded elements is power-bounded in a nonarchimedean ring (Prop 5.30(3)).
Proof for Theorem 2.2
uses 0

Non-archimedeanness gives a neighbourhood basis of 0 by open subgroups, so for an open subgroup U the binomial expansion of (a+b)^n has every term of the form a^i b^{n-i}, each lying in the bounded set generated by the powers of a and b. Choosing U absorbing both \{a^n\} and \{b^n\} and using subadditivity over the subgroup shows \{(a+b)^n\} is absorbed by U. Closure under negation and product is similar, so A^{\circ} is a subring. Following Wedhorn Proposition 5.30(3).

Theorem2.3
uses 1used by 0✓L∃∀N

The power-bounded subring A^{\circ} is integrally closed in A: any element integral over a bounded subring is power-bounded (Definition 2.1). Following Wedhorn Proposition 5.30(4).

Lean code for Theorem2.3●1 theorem
  • theoremdefined in «Adic spaces»/Bounded.lean
    complete
    theorem TopologicalRing.IsBounded.isPowerBounded_of_isIntegral.{u_1}
  {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
  {B : Subring A} (hB : TopologicalRing.IsBounded ↑B) {a : A}
  (ha : IsIntegral (↥B) a) : TopologicalRing.IsPowerBounded a
    theorem TopologicalRing.IsBounded.isPowerBounded_of_isIntegral.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A] {B : Subring A}
  (hB : TopologicalRing.IsBounded ↑B)
  {a : A} (ha : IsIntegral (↥B) a) :
  TopologicalRing.IsPowerBounded a
    `A°` is integrally closed: integral over bounded implies power-bounded (Prop 5.30(4)).
Proof for Theorem 2.3
uses 0

If a satisfies a monic relation a^k = \sum_{i<k} b_i a^i with the b_i in a bounded subring B, then every power a^n is a B-linear combination of 1, a, \dots, a^{k-1}. Boundedness of B and of the finite set \{1, \dots, a^{k-1}\} makes the set of all such combinations bounded, so \{a^n\} is bounded and a \in A^{\circ}. Following Wedhorn Proposition 5.30(4).

Theorem2.4
uses 0used by 1✓L∃∀N

An ideal \mathfrak{a} of a Huber ring is open iff the topological nilradical is contained in its radical, A^{\circ\circ} \subseteq \sqrt{\mathfrak{a}}. Following Wedhorn Lemma 6.6.

Lean code for Theorem2.4●1 theorem
  • theoremdefined in «Adic spaces»/OpenIdeals.lean
    complete
    theorem ideal_isOpen_iff_topologicalNilradical_le_radical.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [IsLinearTopology A A]
  [ContinuousAdd A]
  (hJ :
    ∃ J,
      J.FG ∧ J ≤ topologicalNilradical A ∧ ∀ (n : ℕ), IsOpen ↑(J ^ n))
  (𝔞 : Ideal A) : IsOpen ↑𝔞 ↔ topologicalNilradical A ≤ 𝔞.radical
    theorem ideal_isOpen_iff_topologicalNilradical_le_radical.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsLinearTopology A A] [ContinuousAdd A]
  (hJ :
    ∃ J,
      J.FG ∧
        J ≤ topologicalNilradical A ∧
          ∀ (n : ℕ), IsOpen ↑(J ^ n))
  (𝔞 : Ideal A) :
  IsOpen ↑𝔞 ↔
    topologicalNilradical A ≤ 𝔞.radical
    An ideal is open iff the topological nilradical is in its radical (Lemma 6.6).
Proof for Theorem 2.4
uses 0

(\Rightarrow) If \mathfrak a is open then it contains a neighbourhood of 0, hence a power I^n of a defining ideal, so each topologically nilpotent element has a power in \mathfrak a, giving A^{\circ\circ} \subseteq \sqrt{\mathfrak a}. (\Leftarrow) If the defining ideal I (whose elements are topologically nilpotent) lies in \sqrt{\mathfrak a}, finite generation of I yields a single N with I^N \subseteq \mathfrak a; since I^N is open, so is \mathfrak a. Following Wedhorn Lemma 6.6.