Documentation

TauCeti.Topology.Algebra.TopologicallyNilpotent.Basic

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 #

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 #

source
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.

source
@[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.

source
theorem IsTopologicallyNilpotent.pow {M : Type u_2} [MonoidWithZero M] [TopologicalSpace M] {a : M} (ha : IsTopologicallyNilpotent a) {n : ℕ} (hn : n ≠ 0) :
IsTopologicallyNilpotent (a ^ n)

A positive power of a topologically nilpotent element is topologically nilpotent: the powers of a ^ n are a subsequence of the powers of a.

source
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.

source
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.

source
theorem IsTopologicallyNilpotent.of_pow {M : Type u_2} [MonoidWithZero M] [TopologicalSpace M] [SeparatelyContinuousMul M] {a : M} {m : ℕ} (hm : m ≠ 0) (h : IsTopologicallyNilpotent (a ^ m)) :
IsTopologicallyNilpotent a

An element with a topologically nilpotent positive power is topologically nilpotent.

source
@[simp]
theorem Prod.isTopologicallyNilpotent_iff {M : Type u_2} {N : Type u_3} [MonoidWithZero M] [MonoidWithZero N] [TopologicalSpace M] [TopologicalSpace N] {x : M × N} :
IsTopologicallyNilpotent x ↔ IsTopologicallyNilpotent x.1 ∧ IsTopologicallyNilpotent x.2

An element of a product of topological monoids with zero is topologically nilpotent exactly when both of its components are: the powers of x are taken componentwise, and a sequence in a product converges exactly when both of its component sequences do.

source
theorem IsTopologicallyNilpotent.mem_jacobson_bot {R : Type u_2} [CommRing R] [TopologicalSpace R] {I : Ideal R} (hI : IsOpen ↑I) (hIJ : I ≤ ⊥.jacobson) {a : R} (ha : IsTopologicallyNilpotent a) :
a ∈ ⊥.jacobson

Topologically nilpotent elements lie in the Jacobson radical as soon as some open ideal I does, for instance when R is I-adically complete (IsAdicComplete.le_jacobson): a power of a topologically nilpotent element lies in I, and the Jacobson radical is radical.

source
theorem topologicalNilradical_le_jacobson_bot {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsLinearTopology R R] {I : Ideal R} (hI : IsOpen ↑I) (hIJ : I ≤ ⊥.jacobson) :
topologicalNilradical R ≤ ⊥.jacobson

In a linearly topologized ring, the topological nilradical lies in the Jacobson radical as soon as some open ideal does.

source
theorem IsTopologicallyNilpotent.isUnit_add_left {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsLinearTopology R R] (hR : topologicalNilradical R ≤ ⊥.jacobson) {t u : R} (ht : IsTopologicallyNilpotent t) (hu : IsUnit u) :
IsUnit (u + t)

When the topological nilradical lies in the Jacobson radical (for instance, by topologicalNilradical_le_jacobson_bot), a unit plus a topologically nilpotent element is a unit. Compare IsNilpotent.isUnit_add_left_of_commute.

source
theorem IsTopologicallyNilpotent.prod_one_sub_sub_one {S : Type u_2} [CommRing S] [TopologicalSpace S] [IsLinearTopology S S] {K : Type u_3} [CommRing K] [Algebra K S] {a : S} (ha : IsTopologicallyNilpotent a) (s : Multiset K) :
IsTopologicallyNilpotent ((Multiset.map (fun (μ : K) => 1 - (algebraMap K S) μ * a) s).prod - 1)

For a multiset s of scalars and a topologically nilpotent a, ∏_{μ ∈ s} (1 - μ a) - 1 is topologically nilpotent.