mathlib documentation

ring_theory.nilpotent

Nilpotent elements #

Main definitions #

source
def is_nilpotent {R : Type u} [has_zero R] [has_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 monoid_with_zero is too strong since nilpotency is important in the study of rings that are only power-associative.

Equations
source
theorem is_nilpotent.mk {R : Type u} [has_zero R] [has_pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) :
is_nilpotent x
source
theorem is_nilpotent.zero {R : Type u} [monoid_with_zero R] :
is_nilpotent 0
source
theorem is_nilpotent.neg {R : Type u} {x : R} [ring R] (h : is_nilpotent x) :
is_nilpotent (-x)
source
@[simp]
theorem is_nilpotent_neg_iff {R : Type u} {x : R} [ring R] :
is_nilpotent (-x) ↔ is_nilpotent x
source
theorem is_nilpotent.map {R S : Type u} [monoid_with_zero R] [monoid_with_zero S] {r : R} {F : Type u_1} [monoid_with_zero_hom_class F R S] (hr : is_nilpotent r) (f : F) :
is_nilpotent (⇑f r)
source
@[class]
structure is_reduced (R : Type u_1) [has_zero R] [has_pow R ℕ] :
Prop

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

Instances
source
@[protected, instance]
def is_reduced_of_no_zero_divisors {R : Type u} [monoid_with_zero R] [no_zero_divisors R] :
is_reduced R
source
@[protected, instance]
def is_reduced_of_subsingleton {R : Type u} [has_zero R] [has_pow R ℕ] [subsingleton R] :
is_reduced R
source
theorem is_nilpotent.eq_zero {R : Type u} {x : R} [has_zero R] [has_pow R ℕ] [is_reduced R] (h : is_nilpotent x) :
x = 0
source
@[simp]
theorem is_nilpotent_iff_eq_zero {R : Type u} {x : R} [monoid_with_zero R] [is_reduced R] :
is_nilpotent x ↔ x = 0
source
theorem is_reduced_of_injective {R S : Type u} [monoid_with_zero R] [monoid_with_zero S] {F : Type u_1} [monoid_with_zero_hom_class F R S] (f : F) (hf : function.injective ⇑f) [is_reduced S] :
is_reduced R
source
theorem commute.is_nilpotent_add {R : Type u} {x y : R} [semiring R] (h_comm : commute x y) (hx : is_nilpotent x) (hy : is_nilpotent y) :
is_nilpotent (x + y)
source
theorem commute.is_nilpotent_mul_left {R : Type u} {x y : R} [semiring R] (h_comm : commute x y) (h : is_nilpotent x) :
is_nilpotent (x * y)
source
theorem commute.is_nilpotent_mul_right {R : Type u} {x y : R} [semiring R] (h_comm : commute x y) (h : is_nilpotent y) :
is_nilpotent (x * y)
source
theorem commute.is_nilpotent_sub {R : Type u} {x y : R} [ring R] (h_comm : commute x y) (hx : is_nilpotent x) (hy : is_nilpotent y) :
is_nilpotent (x - y)
source
def nilradical (R : Type u_1) [comm_semiring R] :
ideal R

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

Equations
source
theorem mem_nilradical {R : Type u} {x : R} [comm_semiring R] :
x ∈ nilradical R ↔ is_nilpotent x
source
theorem nilradical_eq_Inf (R : Type u_1) [comm_semiring R] :
nilradical R = Inf {J : ideal R | J.is_prime}
source
theorem nilpotent_iff_mem_prime {R : Type u} {x : R} [comm_semiring R] :
is_nilpotent x ↔ ∀ (J : ideal R), J.is_prime → x ∈ J
source
theorem nilradical_le_prime {R : Type u} [comm_semiring R] (J : ideal R) [H : J.is_prime] :
nilradical R ≤ J
source
@[simp]
theorem nilradical_eq_zero (R : Type u_1) [comm_semiring R] [is_reduced R] :
nilradical R = 0
source
@[simp]
theorem algebra.is_nilpotent_lmul_left_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
is_nilpotent (algebra.lmul_left R a) ↔ is_nilpotent a
source
@[simp]
theorem algebra.is_nilpotent_lmul_right_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
is_nilpotent (algebra.lmul_right R a) ↔ is_nilpotent a
source
theorem module.End.is_nilpotent.mapq {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {f : module.End R M} {p : submodule R M} (hp : p ≤ submodule.comap f p) (hnp : is_nilpotent f) :
is_nilpotent (p.mapq p f hp)