Power-bounded and topologically nilpotent elements

An element of a topological ring is power-bounded when the set of its nonnegative powers is bounded. Following Wedhorn, Adic Spaces, Definitions 5.25 and 5.27, we write

A°  = {a : A | the powers of a are bounded},
A°° = {a : A | aⁿ → 0}

for the power-bounded and the topologically nilpotent elements. Wedhorn Proposition 5.30 says that A° is a subring of A and that A°° is an ideal of A°; both statements need A to be nonarchimedean, that is, to have a neighbourhood basis of zero by additive subgroups. A basis by open ideals would be too strong: a nonzero Tate ring has no proper open ideal.

The subring A° and its transport results do not require continuity of multiplication. Its integral-closure results require separate continuity, and the ideal A°° requires joint continuity.

Provenance

IsPowerBounded, isPowerBounded_zero, isPowerBounded_one, isPowerBounded_mul_of_commute, IsPowerBounded.mul, IsPowerBounded.neg, IsPowerBounded.of_isTopologicallyNilpotent, IsPowerBounded.isTopologicallyNilpotent_mul_of_commute and powerBoundedSubring are stated as in William Coram's mathlib4#40013 (there PowerBounded.subring, and the last two under different names), with weaker assumptions where possible. Further results here include IsPowerBounded.pow, the nonarchimedean IsPowerBounded.add and isTopologicallyNilpotent_add, topologicallyNilpotentIdeal and coe_topologicallyNilpotentIdeal — #40013 carries A°° as a Set.range of an inclusion rather than as an ideal of A° — IsBounded.isPowerBounded_of_mem, and the transport lemmas. The selection and ordering of results follows AINTLIB's Bounded.lean, a prior formalisation of this theory; its proofs were not used.

Claude contributed the algebraic generalization of IsPowerBounded.neg and isPowerBounded_neg from rings to monoids with zero and distributive negation.

Main definitions

• TauCeti.Huber.IsPowerBounded: the powers of a form a bounded set.
• TauCeti.Huber.powerBoundedSubring: the subring A° of power-bounded elements.
• TauCeti.Huber.topologicallyNilpotentIdeal: the ideal A°° of A°.

Main results

• TauCeti.Huber.isPowerBounded_iff: unfolding lemma for IsPowerBounded.
• TauCeti.Huber.isBounded_submonoidClosure and TauCeti.Huber.isBounded_subringClosure (Wedhorn Proposition 5.30(2)): the submonoid, resp. subring, generated by finitely many power-bounded elements is bounded. Neither needs multiplication to be continuous: the empty case is isBounded_pair_zero_one, which is continuity-free, where isBounded_singleton would not be.
• TauCeti.Huber.isPowerBounded_of_isBounded_of_monic: a root of a monic polynomial whose coefficients lie in a bounded subring is power-bounded — the general form behind Wedhorn Proposition 5.30(4).
• TauCeti.Huber.isPowerBounded_of_isIntegral and TauCeti.Huber.isIntegrallyClosedIn_powerBoundedSubring (Wedhorn Proposition 5.30(4)): A° is integrally closed in A, elementwise and as a Mathlib instance.
• TauCeti.Huber.IsPowerBounded.of_isTopologicallyNilpotent: A°° ⊆ A°.
• TauCeti.Huber.isTopologicallyNilpotent_add_of_commute and TauCeti.Huber.isTopologicallyNilpotent_add: commuting topologically nilpotent elements of a nonarchimedean ring have topologically nilpotent sum. Mathlib's IsTopologicallyNilpotent.add instead assumes a basis of open ideals, which excludes the Tate rings this is aimed at.
• TauCeti.Huber.map_powerBoundedSubring, TauCeti.Huber.powerBoundedSubringEquiv: A° is carried onto B° by a topological ring isomorphism, which therefore restricts to A° ≃+* B°; that restriction carries A°° onto B°° (TauCeti.Huber.mem_topologicallyNilpotentIdeal_powerBoundedSubringEquiv_iff pointwise, TauCeti.Huber.map_topologicallyNilpotentIdeal as an equality of ideals).
• TauCeti.Huber.isPowerBounded_ringEquiv_iff, TauCeti.Huber.isTopologicallyNilpotent_ringEquiv_iff: both constructions transport along a topological ring isomorphism.

Implementation notes

topologicallyNilpotentIdeal is an ideal of A°, not of A, and is distinct from Mathlib's topologicalNilradical, which is an ideal of the ring itself under [IsLinearTopology R R]. The present ideal requires a nonarchimedean additive group (NonarchimedeanAddGroup A) and jointly continuous multiplication (ContinuousMul A). The theorem coe_topologicallyNilpotentIdeal records that cutting down to A° loses no topologically nilpotent element.

References

• Wedhorn, Adic Spaces, Definition 5.25, Definition 5.27, Remark 5.28, Proposition 5.30.
• William Coram, feat: define bounded sets and power bounded elements, mathlib4#40013.
• AINTLIB, branch dev/adic-spaces, projects/AdicSpaces/Adic spaces/Bounded.lean.

def TauCeti.Huber.IsPowerBounded {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] (a : M) : Prop

An element is power-bounded if the set of its nonnegative powers is bounded.

Equations

• TauCeti.Huber.IsPowerBounded a = TauCeti.Huber.IsBounded (Set.range fun (x : ℕ) => a ^ x)

theorem TauCeti.Huber.isPowerBounded_iff {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {a : M} : IsPowerBounded a ↔ IsBounded (Set.range fun (x : ℕ) => a ^ x)

Unfolding lemma for TauCeti.Huber.IsPowerBounded.

theorem TauCeti.Huber.IsBounded.isPowerBounded_of_mem {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S : Type u_2} [SetLike S M] [SubmonoidClass S M] {T : S} (hT : IsBounded ↑T) {a : M} (ha : a ∈ T) : IsPowerBounded a

Every element of a bounded submonoid is power-bounded: its powers never leave the submonoid, and the submonoid is absorbed by every neighbourhood of zero. This is the reason a ring of definition, and any other bounded subring, consists of power-bounded elements.

@[simp]

theorem TauCeti.Huber.isPowerBounded_zero {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] : IsPowerBounded 0

0 is power-bounded.

@[simp]

theorem TauCeti.Huber.isPowerBounded_one {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] : IsPowerBounded 1

1 is power-bounded.

theorem TauCeti.Huber.IsPowerBounded.pow {R : Type u_1} [MonoidWithZero R] [TopologicalSpace R] {a : R} (ha : IsPowerBounded a) (m : ℕ) : IsPowerBounded (a ^ m)

A power of a power-bounded element is power-bounded.

theorem TauCeti.Huber.isPowerBounded_mul_of_commute {R : Type u_1} [MonoidWithZero R] [TopologicalSpace R] {a b : R} (hab : Commute a b) (ha : IsPowerBounded a) (hb : IsPowerBounded b) : IsPowerBounded (a * b)

A product of commuting power-bounded elements is power-bounded.

theorem TauCeti.Huber.IsPowerBounded.isTopologicallyNilpotent_mul_of_commute {R : Type u_1} [MonoidWithZero R] [TopologicalSpace R] {a b : R} (hab : Commute a b) (ha : IsPowerBounded a) (hb : IsTopologicallyNilpotent b) : IsTopologicallyNilpotent (a * b)

The product of a power-bounded element with a commuting topologically nilpotent element is topologically nilpotent.

theorem TauCeti.Huber.IsPowerBounded.of_isTopologicallyNilpotent {R : Type u_1} [MonoidWithZero R] [TopologicalSpace R] [ContinuousMul R] {a : R} (ha : IsTopologicallyNilpotent a) : IsPowerBounded a

Topologically nilpotent elements are power-bounded: A°° ⊆ A°.

theorem TauCeti.Huber.IsPowerBounded.mul {R : Type u_1} [CommMonoidWithZero R] [TopologicalSpace R] {a b : R} (ha : IsPowerBounded a) (hb : IsPowerBounded b) : IsPowerBounded (a * b)

A product of power-bounded elements is power-bounded.

theorem TauCeti.Huber.IsPowerBounded.isTopologicallyNilpotent_mul {R : Type u_1} [CommMonoidWithZero R] [TopologicalSpace R] {a b : R} (ha : IsPowerBounded a) (hb : IsTopologicallyNilpotent b) : IsTopologicallyNilpotent (a * b)

The product of a power-bounded element with a topologically nilpotent element is topologically nilpotent.

theorem TauCeti.Huber.IsPowerBounded.neg {A : Type u_1} [MonoidWithZero A] [HasDistribNeg A] [TopologicalSpace A] [ContinuousNeg A] {a : A} (ha : IsPowerBounded a) : IsPowerBounded (-a)

The negative of a power-bounded element is power-bounded.

@[simp]

theorem TauCeti.Huber.isPowerBounded_neg {A : Type u_1} [MonoidWithZero A] [HasDistribNeg A] [TopologicalSpace A] [ContinuousNeg A] {a : A} : IsPowerBounded (-a) ↔ IsPowerBounded a

Power-boundedness is invariant under negation.

theorem TauCeti.Huber.isTopologicallyNilpotent_mk {A : Type u_1} [Ring A] [TopologicalSpace A] {B : Subring A} {x : A} (hx : x ∈ B) (h : IsTopologicallyNilpotent x) : IsTopologicallyNilpotent ⟨x, hx⟩

Topological nilpotence descends to a subring, which carries the subspace topology.

theorem TauCeti.Huber.isBounded_submonoidClosure {A : Type u_1} [CommMonoidWithZero A] [TopologicalSpace A] {C : Set A} (hC : C.Finite) (h : ∀ c ∈ C, IsPowerBounded c) : IsBounded ↑(Submonoid.closure C)

The submonoid generated by finitely many power-bounded elements is bounded: its elements are products of powers of the generators.

theorem TauCeti.Huber.isPowerBounded_of_isBounded_of_mul_mem {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {S : Set A} {x : A} (hS : IsBounded S) (hone : 1 ∈ AddSubgroup.closure S) (hmul : ∀ y ∈ AddSubgroup.closure S, x * y ∈ AddSubgroup.closure S) : IsPowerBounded x

If the additive subgroup generated by a bounded set S contains 1 and is stable under left multiplication by x, then x is power-bounded. Compare IsBounded.isPowerBounded_of_mem, which asks for a bounded submonoid containing x; here neither S nor the additive subgroup it generates need be closed under multiplication.

theorem TauCeti.Huber.IsPowerBounded.add_of_commute {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {a b : A} (hab : Commute a b) (ha : IsPowerBounded a) (hb : IsPowerBounded b) : IsPowerBounded (a + b)

A sum of commuting power-bounded elements is power-bounded in a nonarchimedean ring.

The binomial expansion writes (a + b) ^ n as an integer combination of products aᵏ bᵐ, so the statement follows from IsBounded.addSubgroupClosure. Only a and b need to commute.

theorem TauCeti.Huber.IsPowerBounded.add {A : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {a b : A} (ha : IsPowerBounded a) (hb : IsPowerBounded b) : IsPowerBounded (a + b)

A sum of power-bounded elements of a nonarchimedean commutative ring is power-bounded.

theorem TauCeti.Huber.isTopologicallyNilpotent_add_of_commute {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [ContinuousMul A] {a b : A} (hab : Commute a b) (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) : IsTopologicallyNilpotent (a + b)

A sum of topologically nilpotent elements is topologically nilpotent in a nonarchimedean ring.

Mathlib's IsTopologicallyNilpotent.add assumes a neighbourhood basis of zero by open ideals, which no nonzero Tate ring has; a basis by additive subgroups is enough.

theorem TauCeti.Huber.isTopologicallyNilpotent_add {A : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [ContinuousMul A] {a b : A} (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) : IsTopologicallyNilpotent (a + b)

Over a nonarchimedean commutative ring the topologically nilpotent elements are closed under addition. Mathlib's IsTopologicallyNilpotent.add instead assumes a basis of open ideals, which excludes the Tate rings this is aimed at.

theorem TauCeti.Huber.isBounded_subringClosure {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {C : Set A} (hC : C.Finite) (h : ∀ c ∈ C, IsPowerBounded c) : IsBounded ↑(Subring.closure C)

Wedhorn Proposition 5.30(2): the subring generated by finitely many power-bounded elements is bounded.

theorem TauCeti.Huber.isPowerBounded_of_isBounded_of_monic {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [SeparatelyContinuousMul A] {B : Subring A} (hB : IsBounded ↑B) {p : Polynomial A} (hp : p.Monic) (hcoeff : ∀ (i : ℕ), p.coeff i ∈ B) {x : A} (hroot : Polynomial.eval x p = 0) : IsPowerBounded x

Wedhorn Proposition 5.30(4), general form: a root of a monic polynomial whose coefficients lie in a bounded subring is power-bounded.

Writing n for the degree, the monic relation expresses x ^ n through the lower powers, so all powers of x lie in the additive subgroup generated by B * {1, x, …, x ^ n}; that generating set is bounded, hence so is the subgroup by IsBounded.addSubgroupClosure.

def TauCeti.Huber.powerBoundedSubring (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] : Subring A

The subring A° of power-bounded elements of a nonarchimedean commutative ring (Wedhorn Proposition 5.30). No continuity of multiplication is required.

Equations

• TauCeti.Huber.powerBoundedSubring A = { carrier := {a : A | TauCeti.Huber.IsPowerBounded a}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem TauCeti.Huber.mem_powerBoundedSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {a : A} : a ∈ powerBoundedSubring A ↔ IsPowerBounded a

Membership in A° is power-boundedness.

@[simp]

theorem TauCeti.Huber.coe_powerBoundedSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] : ↑(powerBoundedSubring A) = {a : A | IsPowerBounded a}

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

@[simp]

theorem TauCeti.Huber.powerBoundedSubring_eq_top {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [IsLinearTopology A A] : powerBoundedSubring A = ⊤

In a linearly topologized ring, for instance an adic or a discrete ring, every element is power-bounded, so A° = A.

theorem TauCeti.Huber.isPowerBounded_of_isIntegral {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [SeparatelyContinuousMul A] {x : A} (hx : IsIntegral (↥(powerBoundedSubring A)) x) : IsPowerBounded x

Wedhorn Proposition 5.30(4): the power-bounded subring A° is integrally closed in A.

instance TauCeti.Huber.isIntegrallyClosedIn_powerBoundedSubring {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [SeparatelyContinuousMul A] : IsIntegrallyClosedIn (↥(powerBoundedSubring A)) A

Wedhorn Proposition 5.30(4), as an instance: A° is integrally closed in A. This is the form Mathlib's generic integral-closure API consumes; isPowerBounded_of_isIntegral is the elementwise statement behind it.

def TauCeti.Huber.topologicallyNilpotentIdeal (A : Type u_1) [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [ContinuousMul A] : Ideal ↥(powerBoundedSubring A)

The ideal A°° of topologically nilpotent elements inside A° (Wedhorn Proposition 5.30).

Equations

• TauCeti.Huber.topologicallyNilpotentIdeal A = { carrier := {a : ↥(TauCeti.Huber.powerBoundedSubring A) | IsTopologicallyNilpotent ↑a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.Huber.mem_topologicallyNilpotentIdeal {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [ContinuousMul A] {a : ↥(powerBoundedSubring A)} : a ∈ topologicallyNilpotentIdeal A ↔ IsTopologicallyNilpotent ↑a

Membership in A°° is topological nilpotence.

@[simp]

theorem TauCeti.Huber.coe_topologicallyNilpotentIdeal {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [ContinuousMul A] : Subtype.val '' ↑(topologicallyNilpotentIdeal A) = {a : A | IsTopologicallyNilpotent a}

A°° is exactly the set of topologically nilpotent elements of A: no topologically nilpotent element is lost by cutting down to A°.

theorem TauCeti.Huber.IsPowerBounded.map {M : Type u_1} {N : Type u_2} [MonoidWithZero M] [MonoidWithZero N] [TopologicalSpace M] [TopologicalSpace N] {F : Type u_3} [FunLike F M N] [MonoidWithZeroHomClass F M N] {f : F} (hf : ContinuousAt (⇑f) 0) (hf₀ : ∀ V ∈ nhds 0, ⇑f '' V ∈ nhds 0) {a : M} (ha : IsPowerBounded a) : IsPowerBounded (f a)

A morphism continuous at zero which carries neighbourhoods of zero to neighbourhoods of zero preserves power-boundedness. As for IsBounded.image, continuity at zero alone is not enough.

theorem TauCeti.Huber.IsPowerBounded.map_of_isOpenMap {M : Type u_1} {N : Type u_2} [MonoidWithZero M] [MonoidWithZero N] [TopologicalSpace M] [TopologicalSpace N] {F : Type u_3} [FunLike F M N] [MonoidWithZeroHomClass F M N] {f : F} (hf : ContinuousAt (⇑f) 0) (hf₀ : IsOpenMap ⇑f) {a : M} (ha : IsPowerBounded a) : IsPowerBounded (f a)

An open morphism continuous at zero preserves power-boundedness.

theorem TauCeti.Huber.IsPowerBounded.quotientMk {R : Type u_3} [CommRing R] [TopologicalSpace R] [SeparatelyContinuousAdd R] {a : R} (ha : IsPowerBounded a) (J : Ideal R) : IsPowerBounded ((Ideal.Quotient.mk J) a)

The quotient map R → R ⧸ J preserves power-boundedness. Only continuity of translations is assumed on R, so this applies to every commutative topological ring.

@[simp]

theorem TauCeti.Huber.isPowerBounded_ringEquiv_iff {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) {a : A} : IsPowerBounded (e a) ↔ IsPowerBounded a

Power-boundedness transports along a topological ring isomorphism.

@[simp]

theorem TauCeti.Huber.image_ringEquiv_setOf_isPowerBounded {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : ⇑e '' {a : A | IsPowerBounded a} = {b : B | IsPowerBounded b}

A topological ring isomorphism maps the set of power-bounded elements onto the corresponding set in the target. This set-level result applies to semirings, including when the powerBoundedSubring is not available.

@[simp]

theorem TauCeti.Huber.isTopologicallyNilpotent_ringEquiv_iff {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) {a : A} : IsTopologicallyNilpotent (e a) ↔ IsTopologicallyNilpotent a

Topological nilpotence transports along a topological ring isomorphism.

@[simp]

theorem TauCeti.Huber.map_powerBoundedSubring {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanAddGroup A] [NonarchimedeanAddGroup B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : Subring.map (↑e) (powerBoundedSubring A) = powerBoundedSubring B

A° is preserved by a topological ring isomorphism: e carries A° onto B°. This is the bundled form of TauCeti.Huber.isPowerBounded_ringEquiv_iff.

def TauCeti.Huber.powerBoundedSubringEquiv {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanAddGroup A] [NonarchimedeanAddGroup B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : ↥(powerBoundedSubring A) ≃+* ↥(powerBoundedSubring B)

A topological ring isomorphism restricts to an isomorphism A° ≃+* B°.

Equations

• TauCeti.Huber.powerBoundedSubringEquiv e he he' = e.restrict (TauCeti.Huber.powerBoundedSubring A) (TauCeti.Huber.powerBoundedSubring B) ⋯

@[simp]

theorem TauCeti.Huber.powerBoundedSubringEquiv_apply {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanAddGroup A] [NonarchimedeanAddGroup B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (a : ↥(powerBoundedSubring A)) : ↑((powerBoundedSubringEquiv e he he') a) = e ↑a

theorem TauCeti.Huber.mem_topologicallyNilpotentIdeal_powerBoundedSubringEquiv_iff {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanAddGroup A] [NonarchimedeanAddGroup B] [ContinuousMul A] [ContinuousMul B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) (a : ↥(powerBoundedSubring A)) : (powerBoundedSubringEquiv e he he') a ∈ topologicallyNilpotentIdeal B ↔ a ∈ topologicallyNilpotentIdeal A

A°° is preserved by a topological ring isomorphism: the restricted isomorphism A° ≃+* B° carries A°° exactly onto B°°. See TauCeti.Huber.map_topologicallyNilpotentIdeal for the bundled form.

@[simp]

theorem TauCeti.Huber.map_topologicallyNilpotentIdeal {A : Type u_5} {B : Type u_6} [CommRing A] [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanAddGroup A] [NonarchimedeanAddGroup B] [ContinuousMul A] [ContinuousMul B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : Ideal.map (↑(powerBoundedSubringEquiv e he he')) (topologicallyNilpotentIdeal A) = topologicallyNilpotentIdeal B

The restricted isomorphism A° ≃+* B° carries the ideal A°° onto B°°. This is the bundled form of TauCeti.Huber.mem_topologicallyNilpotentIdeal_powerBoundedSubringEquiv_iff.