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] [Semiring S] [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) :
(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
theorem isNilpotent_iff_zero_mem_powers {R : Type u_1} {x : R} [Monoid R] [Zero R] :
IsNilpotent x ↔ 0 ∈ Submonoid.powers x
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} {x : R} [CommSemiring 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} {x : R} [CommSemiring 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
    theorem nilradical_eq_bot_iff {R : Type u_1} [CommSemiring R] :
    nilradical R = ⊥ ↔ IsReduced R
    source
    theorem Ideal.radical_span_singleton_eq_span_radical {R : Type u_1} {x : R} [CommSemiring R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] (h : x ≠ 0) :
    (span {x}).radical = span {UniqueFactorizationMonoid.radical x}
    source
    @[simp]
    theorem LinearMap.isNilpotent_mulLeft_iff (R : Type u_1) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :
    IsNilpotent (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 (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 : Module.Basis ι R M) (f : M →ₗ[R] M) :
    IsNilpotent ((toMatrix b b) f) ↔ IsNilpotent f
    source
    @[simp]
    theorem Matrix.isNilpotent_toLin'_iff {R : Type u_1} {ι : Type u_3} [DecidableEq ι] [Fintype ι] [CommSemiring R] (A : Matrix ι ι R) :
    IsNilpotent (toLin' A) ↔ IsNilpotent A
    source
    theorem Module.End.isNilpotent_restrict_of_le {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {f : 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 : End R M} {p : Submodule R M} (hp : p ≤ Submodule.comap f p) (hnp : IsNilpotent f) :
    IsNilpotent (p.mapQ p f hp)