Nilpotent elements #

Main definitions #

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

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

Instances For

source

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

IsNilpotent x

source

@[simp]

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

IsNilpotent 0

source

theorem IsNilpotent.neg {R : Type u_1} {x : R} [Ring R] (h : IsNilpotent x) :

IsNilpotent (-x)

source

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

IsNilpotent (x ^ Nat.succ n)

source

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

IsNilpotent (x ^ n)

source

@[simp]

theorem isNilpotent_neg_iff {R : Type u_1} {x : R} [Ring R] :

IsNilpotent (-x) ↔ IsNilpotent x

source

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

IsNilpotent (↑f r)

source

theorem IsNilpotent.sub_one_isUnit {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :

IsUnit (r - 1)

source

theorem Commute.IsNilpotent.add_isUnit {R : Type u_1} [Ring R] {r : R} {u : Rˣ} (hnil : IsNilpotent r) (hru : Commute r ↑u⁻¹) :

IsUnit (↑u + r)

source

theorem isReduced_iff (R : Type u_3) [Zero R] [Pow R ℕ] :

IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0

source

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

Prop

eq_zero : ∀ (x : R), IsNilpotent x → x = 0
A reduced structure has no nonzero nilpotent elements.

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

Instances

source

instance isReduced_of_noZeroDivisors {R : Type u_1} [MonoidWithZero R] [NoZeroDivisors R] :

IsReduced R

Equations

@isReduced_of_noZeroDivisors = @isReduced_of_noZeroDivisors.proof_1

source

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

IsReduced R

Equations

@isReduced_of_subsingleton = @isReduced_of_subsingleton.proof_1

source

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

x = 0

source

@[simp]

theorem isNilpotent_iff_eq_zero {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] :

IsNilpotent x ↔ x = 0

source

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

IsReduced R

source

theorem RingHom.ker_isRadical_iff_reduced_of_surjective {R : Type u_1} {S : Type u_3} {F : Type u_4} [CommSemiring R] [CommRing S] [RingHomClass F R S] {f : F} (hf : Function.Surjective ↑f) :

Ideal.IsRadical (RingHom.ker f) ↔ IsReduced S

source

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

Instances For

source

theorem zero_isRadical_iff {R : Type u_1} [MonoidWithZero R] :

IsRadical 0 ↔ IsReduced R

source

theorem isRadical_iff_span_singleton {R : Type u_1} {y : R} [CommSemiring R] :

IsRadical y ↔ Ideal.IsRadical (Ideal.span {y})

source

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

source

theorem isReduced_iff_pow_one_lt {R : Type u_1} [MonoidWithZero R] (k : ℕ) (hk : 1 < k) :

IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0

source

theorem Commute.isNilpotent_add {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :

IsNilpotent (x + y)

source

theorem Commute.isNilpotent_sum {R : Type u_1} [Semiring R] {ι : Type u_3} {s : Finset ι} {f : ι → R} (hnp : ∀ (i : ι), i ∈ s → IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) :

IsNilpotent (Finset.sum s fun i => f i)

source

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

IsNilpotent (x * y)

source

theorem Commute.isNilpotent_mul_left_iff {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsLeft R) :

IsNilpotent (x * y) ↔ IsNilpotent x

source

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

IsNilpotent (x * y)

source

theorem Commute.isNilpotent_mul_right_iff {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsRight R) :

IsNilpotent (x * y) ↔ IsNilpotent y

source

theorem Commute.isNilpotent_sub {R : Type u_1} {x : R} {y : R} [Ring R] (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :

IsNilpotent (x - y)

source

theorem isNilpotent_sum {R : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → R} (hnp : ∀ (i : ι), i ∈ s → IsNilpotent (f i)) :

IsNilpotent (Finset.sum s fun i => f i)

source

def nilradical (R : Type u_3) [CommSemiring R] :

Ideal R

The nilradical of a commutative semiring is the ideal of nilpotent elements.

Equations

nilradical R = Ideal.radical 0

Instances For

source

theorem mem_nilradical {R : Type u_1} [CommSemiring R] {x : R} :

x ∈ nilradical R ↔ IsNilpotent x

source

theorem nilradical_eq_sInf (R : Type u_3) [CommSemiring R] :

nilradical R = sInf {J | Ideal.IsPrime J}

source

theorem nilpotent_iff_mem_prime {R : Type u_1} [CommSemiring R] {x : R} :

IsNilpotent x ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J

source

theorem nilradical_le_prime {R : Type u_1} [CommSemiring R] (J : Ideal R) [H : Ideal.IsPrime J] :

nilradical R ≤ J

source

@[simp]

theorem nilradical_eq_zero (R : Type u_3) [CommSemiring R] [IsReduced R] :

nilradical R = 0

source

@[simp]

theorem LinearMap.isNilpotent_mulLeft_iff (R : Type u_1) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

IsNilpotent (LinearMap.mulLeft R a) ↔ IsNilpotent a

source

@[simp]

theorem LinearMap.isNilpotent_mulRight_iff (R : Type u_1) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

IsNilpotent (LinearMap.mulRight R a) ↔ IsNilpotent a

source

@[simp]

theorem LinearMap.isNilpotent_toMatrix_iff {R : Type u_1} [CommSemiring R] {ι : Type u_3} {M : Type u_4} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (f : M →ₗ[R] M) :

IsNilpotent (↑(LinearMap.toMatrix b b) f) ↔ IsNilpotent f

source

theorem Module.End.IsNilpotent.mapQ {R : Type u_1} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {f : Module.End R M} {p : Submodule R M} (hp : p ≤ Submodule.comap f p) (hnp : IsNilpotent f) :

IsNilpotent (Submodule.mapQ p p f hp)