Topologically nilpotent elements

Let M be a monoid with zero M, endowed with a topology.

• IsTopologicallyNilpotent a says that a : M is topologically nilpotent, i.e., its powers converge to zero.

• IsTopologicallyNilpotent.map: The image of a topologically nilpotent element under a continuous morphism of monoids with zero endowed with a topology is topologically nilpotent.

• IsTopologicallyNilpotent.zero: 0 is topologically nilpotent.

Let R be a commutative ring with a linear topology.

• IsTopologicallyNilpotent.mul_left: if a : R is topologically nilpotent, then a*b is topologically nilpotent.

• IsTopologicallyNilpotent.mul_right: if a : R is topologically nilpotent, then a * b is topologically nilpotent.

• IsTopologicallyNilpotent.add: if a b : R are topologically nilpotent, then a + b is topologically nilpotent.

These lemmas are actually deduced from their analogues for commuting elements of rings.

def IsTopologicallyNilpotent {R : Type u_1} [MonoidWithZero R] [TopologicalSpace R] (a : R) : Prop

An element is topologically nilpotent if its powers converge to 0.

theorem IsTopologicallyNilpotent.map {R : Type u_1} {S : Type u_2} [TopologicalSpace R] [MonoidWithZero R] [MonoidWithZero S] [TopologicalSpace S] {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] {φ : F} (hφ : Continuous ⇑φ) {a : R} (ha : IsTopologicallyNilpotent a) : IsTopologicallyNilpotent (φ a)

The image of a topologically nilpotent element under a continuous morphism is topologically nilpotent

theorem IsTopologicallyNilpotent.zero {R : Type u_1} [TopologicalSpace R] [MonoidWithZero R] : IsTopologicallyNilpotent 0

0 is topologically nilpotent

theorem IsNilpotent.isTopologicallyNilpotent {R : Type u_1} [TopologicalSpace R] [MonoidWithZero R] {a : R} (ha : IsNilpotent a) : IsTopologicallyNilpotent a

theorem IsTopologicallyNilpotent.exists_pow_mem_of_mem_nhds {R : Type u_1} [TopologicalSpace R] [MonoidWithZero R] {a : R} (ha : IsTopologicallyNilpotent a) {v : Set R} (hv : v ∈ nhds 0) : ∃ (n : ℕ), a ^ n ∈ v

theorem IsTopologicallyNilpotent.mul_right_of_commute {R : Type u_1} [TopologicalSpace R] [Ring R] [IsLinearTopology Rᵐᵒᵖ R] {a b : R} (ha : IsTopologicallyNilpotent a) (hab : Commute a b) : IsTopologicallyNilpotent (a * b)

If a and b commute and a is topologically nilpotent, then a * b is topologically nilpotent.

theorem IsTopologicallyNilpotent.mul_left_of_commute {R : Type u_1} [TopologicalSpace R] [Ring R] [IsLinearTopology R R] {a b : R} (hb : IsTopologicallyNilpotent b) (hab : Commute a b) : IsTopologicallyNilpotent (a * b)

If a and b commute and b is topologically nilpotent, then a * b is topologically nilpotent.

theorem IsTopologicallyNilpotent.add_of_commute {R : Type u_1} [TopologicalSpace R] [Ring R] [IsLinearTopology R R] {a b : R} (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) (h : Commute a b) : IsTopologicallyNilpotent (a + b)

If a and b are topologically nilpotent and commute, then a + b is topologically nilpotent.

theorem IsTopologicallyNilpotent.mul_right {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsLinearTopology R R] {a : R} (ha : IsTopologicallyNilpotent a) (b : R) : IsTopologicallyNilpotent (a * b)

If a is topologically nilpotent, then a * b is topologically nilpotent.

theorem IsTopologicallyNilpotent.mul_left {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsLinearTopology R R] (a : R) {b : R} (hb : IsTopologicallyNilpotent b) : IsTopologicallyNilpotent (a * b)

If b is topologically nilpotent, then a * b is topologically nilpotent.

theorem IsTopologicallyNilpotent.add {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsLinearTopology R R] {a b : R} (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) : IsTopologicallyNilpotent (a + b)

If a and b are topologically nilpotent, then a + b is topologically nilpotent.

def topologicalNilradical (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsLinearTopology R R] : Ideal R

The topological nilradical of a ring with a linear topology

@[simp]

theorem coe_topologicalNilradical (R : Type u_1) [TopologicalSpace R] [CommRing R] [IsLinearTopology R R] : ↑(topologicalNilradical R) = {a : R | IsTopologicallyNilpotent a}

theorem IsTopologicallyNilpotent.mem_topologicalNilradical_iff {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsLinearTopology R R] {a : R} : a ∈ topologicalNilradical R ↔ IsTopologicallyNilpotent a