Definition of nilpotent elements

This file defines the notion of a nilpotent element and proves the immediate consequences. For results that require further theory, see Mathlib.RingTheory.Nilpotent.Basic and Mathlib.RingTheory.Nilpotent.Lemmas.

Main definitions

• IsNilpotent
• Commute.isNilpotent_mul_left
• Commute.isNilpotent_mul_right
• nilpotencyClass

def IsNilpotent {R : Type u_1} [Zero R] [Pow R ℕ] (x : R) : Prop

An element is said to be nilpotent if some natural-number-power of it equals zero.

Note that we require only the bare minimum assumptions for the definition to make sense. Even MonoidWithZero is too strong since nilpotency is important in the study of rings that are only power-associative.

Equations

• IsNilpotent x = ∃ (n : ℕ), x ^ n = 0

theorem IsNilpotent.mk {R : Type u_1} [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) : IsNilpotent x

@[simp]

theorem isNilpotent_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] : IsNilpotent x

@[simp]

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

theorem not_isNilpotent_one {R : Type u_1} [MonoidWithZero R] [Nontrivial R] : ¬IsNilpotent 1

theorem IsNilpotent.pow_succ (n : ℕ) {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ)

theorem IsNilpotent.of_pow {R : Type u_1} [MonoidWithZero R] {x : R} {m : ℕ} (h : IsNilpotent (x ^ m)) : IsNilpotent x

theorem IsNilpotent.pow_of_pos {n : ℕ} {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) (hn : n ≠ 0) : IsNilpotent (x ^ n)

@[simp]

theorem IsNilpotent.pow_iff_pos {n : ℕ} {S : Type u_3} [MonoidWithZero S] {x : S} (hn : n ≠ 0) : IsNilpotent (x ^ n) ↔ IsNilpotent x

theorem IsNilpotent.map {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] (hr : IsNilpotent r) (f : F) : IsNilpotent (f r)

theorem IsNilpotent.map_iff {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective ⇑f) : IsNilpotent (f r) ↔ IsNilpotent r

theorem IsUnit.isNilpotent_mul_unit_of_commute_iff {R : Type u_1} [MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) : IsNilpotent (r * u) ↔ IsNilpotent r

theorem IsUnit.isNilpotent_unit_mul_of_commute_iff {R : Type u_1} [MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) : IsNilpotent (u * r) ↔ IsNilpotent r

noncomputable def nilpotencyClass {R : Type u_1} (x : R) [Zero R] [Pow R ℕ] : ℕ

If x is nilpotent, the nilpotency class is the smallest natural number k such that x ^ k = 0. If x is not nilpotent, the nilpotency class takes the junk value 0.

Equations

• nilpotencyClass x = sInf {k : ℕ | x ^ k = 0}

@[simp]

theorem nilpotencyClass_eq_zero_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] : nilpotencyClass x = 0

theorem isNilpotent_of_pos_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] (hx : 0 < nilpotencyClass x) : IsNilpotent x

theorem pow_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] (hx : IsNilpotent x) : x ^ nilpotencyClass x = 0

theorem nilpotencyClass_eq_succ_iff {R : Type u_1} {x : R} [MonoidWithZero R] {k : ℕ} : nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

@[simp]

theorem nilpotencyClass_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] : nilpotencyClass 0 = 1

@[simp]

theorem pos_nilpotencyClass_iff {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] : 0 < nilpotencyClass x ↔ IsNilpotent x

theorem pow_pred_nilpotencyClass {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] (hx : IsNilpotent x) : x ^ (nilpotencyClass x - 1) ≠ 0

theorem eq_zero_of_nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] (hx : nilpotencyClass x = 1) : x = 0

@[simp]

theorem nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] : nilpotencyClass x = 1 ↔ x = 0

class IsReduced (R : Type u_3) [Zero R] [Pow R ℕ] : Prop

A structure that has zero and pow is reduced if it has no nonzero nilpotent elements.

• eq_zero : ∀ (x : R), IsNilpotent x → x = 0

  A reduced structure has no nonzero nilpotent elements.

theorem isReduced_iff (R : Type u_3) [Zero R] [Pow R ℕ] : IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0

theorem IsReduced.pow_eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) : x = 0

@[simp]

theorem IsReduced.pow_eq_zero_iff {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) : x ^ n = 0 ↔ x = 0

theorem IsReduced.pow_ne_zero_iff {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) : x ^ n ≠ 0 ↔ x ≠ 0

theorem IsReduced.pow_ne_zero {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] (n : ℕ) (h : x ≠ 0) : x ^ n ≠ 0

@[simp]

theorem IsReduced.pow_eq_zero_iff' {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} : x ^ n = 0 ↔ x = 0 ∧ n ≠ 0

A variant of IsReduced.pow_eq_zero_iff assuming R is not trivial.

theorem isReduced_of_noZeroDivisors {R : Type u_1} [MonoidWithZero R] [NoZeroDivisors R] : IsReduced R

theorem isReduced_of_subsingleton {R : Type u_1} [Zero R] [Pow R ℕ] [Subsingleton R] : IsReduced R

theorem IsNilpotent.eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] (h : IsNilpotent x) : x = 0

@[simp]

theorem isNilpotent_iff_eq_zero {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] : IsNilpotent x ↔ x = 0

theorem isReduced_of_injective {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] (f : F) (hf : Function.Injective ⇑f) [IsReduced S] : IsReduced R

theorem instIsReducedForall (ι : Type u_4) (R : ι → Type u_3) [(i : ι) → Zero (R i)] [(i : ι) → Pow (R i) ℕ] [∀ (i : ι), IsReduced (R i)] : IsReduced ((i : ι) → R i)

def IsRadical {R : Type u_1} [Dvd R] [Pow R ℕ] (y : R) : Prop

An element y in a monoid is radical if for any element x, y divides x whenever it divides a power of x.

Equations

• IsRadical y = ∀ (n : ℕ) (x : R), y ∣ x ^ n → y ∣ x

theorem isRadical_iff_pow_one_lt {R : Type u_1} {y : R} [MonoidWithZero R] (k : ℕ) (hk : 1 < k) : IsRadical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x

theorem Commute.isNilpotent_mul_left {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent x) : IsNilpotent (x * y)

theorem Commute.isNilpotent_mul_right {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent y) : IsNilpotent (x * y)