Mathlib.RingTheory.Nilpotent.Lemmas

RingHom.ker_isRadical_iff_reduced_of_surjective theorem

 {S F} [CommSemiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) :
  (RingHom.ker f).IsRadical ↔ IsReduced S

Full source

theorem RingHom.ker_isRadical_iff_reduced_of_surjective {S F} [CommSemiring R] [Semiring S]
    [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) :
    (RingHom.ker f).IsRadical ↔ IsReduced S := by
  simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]
  rfl

Kernel is Radical iff Codomain is Reduced for Surjective Ring Homomorphism

Informal description

Let $R$ be a commutative semiring and $S$ a semiring. Given a surjective ring homomorphism $f : R \to S$, the kernel of $f$ is a radical ideal if and only if $S$ is reduced (i.e., has no nonzero nilpotent elements).

isRadical_iff_span_singleton theorem

[CommSemiring R] : IsRadical y ↔ (Ideal.span ({ y } : Set R)).IsRadical

Full source

theorem isRadical_iff_span_singleton [CommSemiring R] :
    IsRadicalIsRadical y ↔ (Ideal.span ({y} : Set R)).IsRadical := by
  simp_rw [IsRadical, ← Ideal.mem_span_singleton]
  exact forall_swap.trans (forall_congr' fun r => exists_imp.symm)

Characterization of Radical Elements via Generated Ideals

Informal description

For any element $y$ in a commutative semiring $R$, $y$ is radical if and only if the ideal generated by $\{y\}$ is a radical ideal.

isNilpotent_iff_zero_mem_powers theorem

[Monoid R] [Zero R] {x : R} : IsNilpotent x ↔ 0 ∈ Submonoid.powers x

Full source

theorem isNilpotent_iff_zero_mem_powers [Monoid R] [Zero R] {x : R} :
    IsNilpotentIsNilpotent x ↔ 0 ∈ Submonoid.powers x := Iff.rfl

Nilpotency Criterion via Powers Submonoid

Informal description

An element $x$ of a monoid $R$ with a zero element is nilpotent if and only if zero belongs to the submonoid generated by the powers of $x$, i.e., $0 \in \{x^k \mid k \in \mathbb{N}\}$.

nilradical definition

(R : Type*) [CommSemiring R] : Ideal R

Full source

/-- The nilradical of a commutative semiring is the ideal of nilpotent elements. -/
def nilradical (R : Type*) [CommSemiring R] : Ideal R :=
  (0 : Ideal R).radical

Nilradical of a commutative semiring

Informal description

The nilradical of a commutative semiring $R$ is the ideal consisting of all nilpotent elements of $R$. It can be characterized as the radical of the zero ideal, or equivalently as the intersection of all prime ideals in $R$.

mem_nilradical theorem

: x ∈ nilradical R ↔ IsNilpotent x

Full source

theorem mem_nilradical : x ∈ nilradical Rx ∈ nilradical R ↔ IsNilpotent x :=
  Iff.rfl

Characterization of Nilradical Membership via Nilpotency

Informal description

An element $x$ of a commutative semiring $R$ belongs to the nilradical of $R$ if and only if $x$ is nilpotent, i.e., there exists a natural number $n$ such that $x^n = 0$.

nilradical_eq_sInf theorem

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

Full source

theorem nilradical_eq_sInf (R : Type*) [CommSemiring R] :
    nilradical R = sInf { J : Ideal R | J.IsPrime } :=
  (Ideal.radical_eq_sInf ⊥).trans <| by simp_rw [and_iff_right bot_le]

Nilradical as Intersection of Prime Ideals

Informal description

For a commutative semiring $R$, the nilradical of $R$ is equal to the infimum of all prime ideals in $R$, i.e., \[ \text{nilradical}(R) = \bigcap \{ J \subseteq R \mid J \text{ is a prime ideal} \}. \]

nilpotent_iff_mem_prime theorem

: IsNilpotent x ↔ ∀ J : Ideal R, J.IsPrime → x ∈ J

Full source

theorem nilpotent_iff_mem_prime : IsNilpotentIsNilpotent x ↔ ∀ J : Ideal R, J.IsPrime → x ∈ J := by
  rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]
  rfl

Nilpotent Elements Belong to All Prime Ideals

Informal description

An element $x$ of a commutative semiring $R$ is nilpotent if and only if $x$ belongs to every prime ideal $J$ of $R$. In other words, $x^n = 0$ for some natural number $n$ if and only if $x \in J$ for all prime ideals $J$ of $R$.

nilradical_le_prime theorem

(J : Ideal R) [H : J.IsPrime] : nilradical R ≤ J

Full source

theorem nilradical_le_prime (J : Ideal R) [H : J.IsPrime] : nilradical R ≤ J :=
  (nilradical_eq_sInf R).symm ▸ sInf_le H

Nilradical is Contained in Every Prime Ideal

Informal description

For any prime ideal $J$ in a commutative semiring $R$, the nilradical of $R$ is contained in $J$, i.e., $\text{nilradical}(R) \subseteq J$.

nilradical_eq_zero theorem

(R : Type*) [CommSemiring R] [IsReduced R] : nilradical R = 0

Full source

@[simp]
theorem nilradical_eq_zero (R : Type*) [CommSemiring R] [IsReduced R] : nilradical R = 0 :=
  Ideal.ext fun _ => isNilpotent_iff_eq_zero

Nilradical Vanishes in Reduced Commutative Semirings: $\text{nilradical}(R) = 0$

Informal description

For any commutative semiring $R$ that is reduced (i.e., has no nonzero nilpotent elements), the nilradical of $R$ is equal to the zero ideal, i.e., $\text{nilradical}(R) = 0$.

nilradical_eq_bot_iff theorem

{R : Type*} [CommSemiring R] : nilradical R = ⊥ ↔ IsReduced R

Full source

theorem nilradical_eq_bot_iff {R : Type*} [CommSemiring R] : nilradicalnilradical R = ⊥ ↔ IsReduced R := by
  simp_rw [eq_bot_iff, SetLike.le_def, Submodule.mem_bot, mem_nilradical, isReduced_iff]

Nilradical Vanishes if and only if Semiring is Reduced

Informal description

For a commutative semiring $R$, the nilradical of $R$ is equal to the zero ideal if and only if $R$ is reduced (i.e., has no nonzero nilpotent elements). In other words, $\text{nilradical}(R) = 0 \leftrightarrow \text{IsReduced}(R)$.

LinearMap.isNilpotent_mulLeft_iff theorem

(a : A) : IsNilpotent (mulLeft R a) ↔ IsNilpotent a

Full source

@[simp]
theorem isNilpotent_mulLeft_iff (a : A) : IsNilpotentIsNilpotent (mulLeft R a) ↔ IsNilpotent a := by
  constructor <;> rintro ⟨n, hn⟩ <;> use n <;>
      simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢ <;>
    exact hn

Nilpotency of Left Multiplication Map vs. Element

Informal description

For any element $a$ in an algebra $A$ over a commutative semiring $R$, the left multiplication map $\text{mulLeft}_R(a)$ is nilpotent if and only if $a$ itself is nilpotent.

LinearMap.isNilpotent_mulRight_iff theorem

(a : A) : IsNilpotent (mulRight R a) ↔ IsNilpotent a

Full source

@[simp]
theorem isNilpotent_mulRight_iff (a : A) : IsNilpotentIsNilpotent (mulRight R a) ↔ IsNilpotent a := by
  constructor <;> rintro ⟨n, hn⟩ <;> use n <;>
      simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢ <;>
    exact hn

Nilpotency of Right Multiplication Map vs. Element in Algebra

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any element $a \in A$, the right multiplication map $\text{mulRight}_R(a)$ is nilpotent if and only if $a$ is nilpotent.

LinearMap.isNilpotent_toMatrix_iff theorem

(b : Basis ι R M) (f : M →ₗ[R] M) : IsNilpotent (toMatrix b b f) ↔ IsNilpotent f

Full source

@[simp]
lemma isNilpotent_toMatrix_iff (b : Basis ι R M) (f : M →ₗ[R] M) :
    IsNilpotentIsNilpotent (toMatrix b b f) ↔ IsNilpotent f := by
  refine exists_congr fun k ↦ ?_
  rw [toMatrix_pow]
  exact (toMatrix b b).map_eq_zero_iff

Nilpotency of Linear Endomorphism and Its Matrix Representation

Informal description

Let $R$ be a commutative ring, $M$ be a finite free $R$-module with basis $b$, and $f : M \to M$ be a linear endomorphism. Then the matrix representation of $f$ with respect to $b$ is nilpotent if and only if $f$ itself is nilpotent. In other words, for any basis $b$ of $M$, we have: \[ \text{IsNilpotent}(A) \leftrightarrow \text{IsNilpotent}(f) \] where $A$ is the matrix representation of $f$ with respect to $b$.

Module.End.isNilpotent_restrict_of_le theorem

 {f : End R M} {p q : Submodule R M} {hp : MapsTo f p p} {hq : MapsTo f q q} (h : p ≤ q)
  (hf : IsNilpotent (f.restrict hq)) : IsNilpotent (f.restrict hp)

Full source

lemma isNilpotent_restrict_of_le {f : End R M} {p q : Submodule R M}
    {hp : MapsTo f p p} {hq : MapsTo f q q} (h : p ≤ q) (hf : IsNilpotent (f.restrict hq)) :
    IsNilpotent (f.restrict hp) := by
  obtain ⟨n, hn⟩ := hf
  use n
  ext ⟨x, hx⟩
  replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩
  simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢
  rw [Module.End.pow_restrict, LinearMap.restrict_apply] at hn ⊢
  ext
  exact (congr_arg Subtype.val hn :)

Nilpotency of Restricted Endomorphism on Smaller Submodule

Informal description

Let $R$ be a ring and $M$ an $R$-module. Let $f$ be an endomorphism of $M$, and let $p$ and $q$ be submodules of $M$ such that $f$ maps $p$ into $p$ and $q$ into $q$. If $p \subseteq q$ and the restriction of $f$ to $q$ is nilpotent, then the restriction of $f$ to $p$ is also nilpotent.

Module.End.isNilpotent.restrict theorem

{f : M →ₗ[R] M} {p : Submodule R M} (hf : MapsTo f p p) (hnil : IsNilpotent f) : IsNilpotent (f.restrict hf)

Full source

lemma isNilpotent.restrict
    {f : M →ₗ[R] M} {p : Submodule R M} (hf : MapsTo f p p) (hnil : IsNilpotent f) :
    IsNilpotent (f.restrict hf) := by
  obtain ⟨n, hn⟩ := hnil
  exact ⟨n, LinearMap.ext fun m ↦ by simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]; rfl⟩

Nilpotency of Restricted Linear Endomorphism

Informal description

Let $f$ be a nilpotent linear endomorphism of an $R$-module $M$, and let $p$ be a submodule of $M$ such that $f$ maps $p$ into itself. Then the restriction of $f$ to $p$ is also nilpotent.

Module.End.IsNilpotent.mapQ theorem

(hnp : IsNilpotent f) : IsNilpotent (p.mapQ p f hp)

Full source

theorem IsNilpotent.mapQ (hnp : IsNilpotent f) : IsNilpotent (p.mapQ p f hp) := by
  obtain ⟨k, hk⟩ := hnp
  use k
  simp [← p.mapQ_pow, hk]

Nilpotency of Induced Endomorphism on Quotient Module

Informal description

Let $R$ be a ring and $M$ an $R$-module. Let $f \colon M \to M$ be a nilpotent linear endomorphism, and let $p$ be a submodule of $M$ such that $f$ maps $p$ into itself. Then the induced linear map $f \colon M ⧸ p \to M ⧸ p$ on the quotient module is also nilpotent.