Nilpotent elements

This file contains results about nilpotent elements that involve ring theory.

theorem RingHom.ker_isRadical_iff_reduced_of_surjective {R : Type u_1} {S : Type u_3} {F : Type u_4} [CommSemiring R] [CommRing S] [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) : (RingHom.ker f).IsRadical ↔ IsReduced S

theorem isRadical_iff_span_singleton {R : Type u_1} {y : R} [CommSemiring R] : IsRadical y ↔ (Ideal.span {y}).IsRadical

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

theorem mem_nilradical {R : Type u_1} [CommSemiring R] {x : R} : x ∈ nilradical R ↔ IsNilpotent x

theorem nilradical_eq_sInf (R : Type u_3) [CommSemiring R] : nilradical R = sInf {J : Ideal R | J.IsPrime}

theorem nilpotent_iff_mem_prime {R : Type u_1} [CommSemiring R] {x : R} : IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

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

@[simp]

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

@[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

@[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

@[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

theorem Module.End.isNilpotent_restrict_of_le {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} {p q : Submodule R M} {hp : Set.MapsTo ⇑f ↑p ↑p} {hq : Set.MapsTo ⇑f ↑q ↑q} (h : p ≤ q) (hf : IsNilpotent (LinearMap.restrict f hq)) : IsNilpotent (LinearMap.restrict f hp)

theorem Module.End.isNilpotent.restrict {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] M} {p : Submodule R M} (hf : Set.MapsTo ⇑f ↑p ↑p) (hnil : IsNilpotent f) : IsNilpotent (f.restrict hf)

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 (p.mapQ p f hp)