scilib documentation

ring_theory.nilpotent

Nilpotent elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
theorem is_reduced_iff (R : Type u_1) [has_zero R] [has_pow R ℕ] :
is_reduced R ↔ ∀ (x : R), is_nilpotent x → x = 0
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 of this typeclass
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 ring_hom.ker_is_radical_iff_reduced_of_surjective {R : Type u} {S : Type u_1} {F : Type u_2} [comm_semiring R] [comm_ring S] [ring_hom_class F R S] {f : F} (hf : function.surjective ⇑f) :
(ring_hom.ker f).is_radical ↔ is_reduced S
source
def is_radical {R : Type u} [has_dvd R] [has_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
source
theorem zero_is_radical_iff {R : Type u} [monoid_with_zero R] :
is_radical 0 ↔ is_reduced R
source
theorem is_radical_iff_span_singleton {R : Type u} {y : R} [comm_semiring R] :
is_radical y ↔ (ideal.span {y}).is_radical
source
theorem is_radical_iff_pow_one_lt {R : Type u} {y : R} [monoid_with_zero R] (k : ℕ) (hk : 1 < k) :
is_radical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x
source
theorem is_reduced_iff_pow_one_lt {R : Type u} [monoid_with_zero R] (k : ℕ) (hk : 1 < k) :
is_reduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
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 = has_Inf.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 linear_map.is_nilpotent_mul_left_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
is_nilpotent (linear_map.mul_left R a) ↔ is_nilpotent a
source
@[simp]
theorem linear_map.is_nilpotent_mul_right_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
is_nilpotent (linear_map.mul_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)