Documentation

Mathlib.RingTheory.Nilpotent.Lemmas

Nilpotent elements #

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

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] [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) :
(RingHom.ker f).IsRadical ↔ IsReduced S
source
theorem isRadical_iff_span_singleton {R : Type u_1} {y : R} [CommSemiring R] :
IsRadical y ↔ (Ideal.span {y}).IsRadical
source
def nilradical (R : Type u_3) [CommSemiring R] :
Ideal R

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

Equations
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 R | J.IsPrime}
    source
    theorem nilpotent_iff_mem_prime {R : Type u_1} [CommSemiring R] {x : R} :
    IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
    source
    theorem nilradical_le_prime {R : Type u_1} [CommSemiring R] (J : Ideal R) [H : J.IsPrime] :
    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_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)
    source
    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)
    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 (p.mapQ p f hp)