Negation and topological nilpotence

Mathlib closes IsTopologicallyNilpotent under the operations that a topology on the ring makes available — zero, add, mul_left, mul_right, map — but not under negation. This file adds that, at the hypotheses the statement needs: a MonoidWithZero with a distributive negation, and continuity of negation.

No uniformity, nonarchimedean neighbourhood basis or commutativity is involved. (-a) ^ n is a ^ n for even n and -(a ^ n) for odd n, and both of those sequences tend to 0 as soon as negation is continuous, so every neighbourhood of 0 eventually contains (-a) ^ n whichever parity n has.

Main results

• IsTopologicallyNilpotent.neg : the negation of a topologically nilpotent element is topologically nilpotent.
• isTopologicallyNilpotent_neg : the same fact as a simp iff, mirroring isPowerBounded_neg.
• eventually_mul_pow_mem_of_isTopologicallyNilpotent, and its .exists form: a topologically nilpotent element absorbs any fixed element into any open subring.

Provenance

The statement is AINTLIB's IsTopologicallyNilpotent.neg, branch dev/adic-spaces, commit 37bbdaeb, Apache-2.0, Chris Birkbeck, projects/AdicSpaces/Adic spaces/GeometricSeries.lean. There it sits inside the geometric-series development over a complete nonarchimedean uniform commutative ring, and the sign on the odd powers is absorbed by an open subgroup. Only the statement is followed here: the hypotheses are weakened to the ones the result needs, and the open-subgroup step is replaced by the two-sequence argument above, which needs no nonarchimedean basis. The iff form has no counterpart in the source.

References

• C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb, projects/AdicSpaces/Adic spaces/GeometricSeries.lean.

theorem IsTopologicallyNilpotent.neg {R : Type u_1} [MonoidWithZero R] [HasDistribNeg R] [TopologicalSpace R] [ContinuousNeg R] {a : R} (ha : IsTopologicallyNilpotent a) : IsTopologicallyNilpotent (-a)

The negation of a topologically nilpotent element is topologically nilpotent.

@[simp]

theorem isTopologicallyNilpotent_neg {R : Type u_1} [MonoidWithZero R] [HasDistribNeg R] [TopologicalSpace R] [ContinuousNeg R] {a : R} : IsTopologicallyNilpotent (-a) ↔ IsTopologicallyNilpotent a

Topological nilpotence is invariant under negation.

theorem eventually_mul_pow_mem_of_isTopologicallyNilpotent {A : Type u_2} [Ring A] [TopologicalSpace A] [SeparatelyContinuousMul A] {s : A} (hs : IsTopologicallyNilpotent s) {B : Subring A} (hB : IsOpen ↑B) (a : A) : ∀ᶠ (n : ℕ) in Filter.atTop, a * s ^ n ∈ B

A topologically nilpotent element absorbs any element into any open subring. For s topologically nilpotent and B open, a * s ^ n lies in B for all large n.

Multiplication by a is continuous, so B pulls back to a neighbourhood of 0, and the powers of s converge to 0. Neither commutativity nor continuity of addition is used — only SeparatelyContinuousMul — and no Huber structure enters, which is why this sits here rather than beside the ring-of-definition form it generalises, TauCeti.Huber.PairOfDefinition.exists_pow_idealOfDefinition_mul_mem.

theorem exists_mul_pow_mem_of_isTopologicallyNilpotent {A : Type u_2} [Ring A] [TopologicalSpace A] [SeparatelyContinuousMul A] {s : A} (hs : IsTopologicallyNilpotent s) {B : Subring A} (hB : IsOpen ↑B) (a : A) : ∃ (n : ℕ), a * s ^ n ∈ B

The existential form of eventually_mul_pow_mem_of_isTopologicallyNilpotent: some power of a topologically nilpotent element carries a into an open subring.