Mathlib.RingTheory.Nilpotent.Basic

IsNilpotent.neg theorem

[Ring R] (h : IsNilpotent x) : IsNilpotent (-x)

Full source

theorem IsNilpotent.neg [Ring R] (h : IsNilpotent x) : IsNilpotent (-x) := by
  obtain ⟨n, hn⟩ := h
  use n
  rw [neg_pow, hn, mul_zero]

Negation preserves nilpotency in rings

Informal description

Let $R$ be a ring and $x \in R$ be a nilpotent element. Then $-x$ is also nilpotent.

isNilpotent_neg_iff theorem

[Ring R] : IsNilpotent (-x) ↔ IsNilpotent x

Full source

@[simp]
theorem isNilpotent_neg_iff [Ring R] : IsNilpotentIsNilpotent (-x) ↔ IsNilpotent x :=
  ⟨fun h => neg_neg x ▸ h.neg, fun h => h.neg⟩

Negation Preserves Nilpotency in Rings: $-x$ nilpotent $\iff$ $x$ nilpotent

Informal description

Let $R$ be a ring and $x \in R$. Then $-x$ is nilpotent if and only if $x$ is nilpotent.

IsNilpotent.smul theorem

 [MonoidWithZero R] [MonoidWithZero S] [MulActionWithZero R S] [SMulCommClass R S S] [IsScalarTower R S S] {a : S}
  (ha : IsNilpotent a) (t : R) : IsNilpotent (t • a)

Full source

lemma IsNilpotent.smul [MonoidWithZero R] [MonoidWithZero S] [MulActionWithZero R S]
    [SMulCommClass R S S] [IsScalarTower R S S] {a : S} (ha : IsNilpotent a) (t : R) :
    IsNilpotent (t • a) := by
  obtain ⟨k, ha⟩ := ha
  use k
  rw [smul_pow, ha, smul_zero]

Scalar Multiplication Preserves Nilpotency

Informal description

Let $R$ and $S$ be monoids with zero, with $S$ being a multiplicative $R$-action with zero where the actions commute and form a scalar tower. For any nilpotent element $a \in S$ and any scalar $t \in R$, the scalar multiple $t \cdot a$ is also nilpotent.

IsNilpotent.isUnit_sub_one theorem

[Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r - 1)

Full source

theorem IsNilpotent.isUnit_sub_one [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r - 1) := by
  obtain ⟨n, hn⟩ := hnil
  refine ⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩
  · simp [mul_geom_sum, hn]
  · simp [geom_sum_mul, hn]

Nilpotent Elements Yield Units via Subtraction: $r$ nilpotent $\Rightarrow$ $r-1$ is a unit

Informal description

Let $R$ be a ring and $r \in R$ be a nilpotent element. Then $r - 1$ is a unit in $R$.

IsNilpotent.isUnit_one_sub theorem

[Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (1 - r)

Full source

theorem IsNilpotent.isUnit_one_sub [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (1 - r) := by
  rw [← IsUnit.neg_iff, neg_sub]
  exact isUnit_sub_one hnil

Nilpotent Elements Yield Units via One Minus: $r$ nilpotent $\Rightarrow$ $1-r$ is a unit

Informal description

Let $R$ be a ring and $r \in R$ be a nilpotent element. Then $1 - r$ is a unit in $R$.

IsNilpotent.isUnit_add_one theorem

[Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r + 1)

Full source

theorem IsNilpotent.isUnit_add_one [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r + 1) := by
  rw [← IsUnit.neg_iff, neg_add']
  exact isUnit_sub_one hnil.neg

Nilpotent Elements Yield Units via Addition: $r$ nilpotent $\Rightarrow$ $r+1$ is a unit

Informal description

Let $R$ be a ring and $r \in R$ be a nilpotent element. Then $r + 1$ is a unit in $R$.

IsNilpotent.isUnit_one_add theorem

[Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (1 + r)

Full source

theorem IsNilpotent.isUnit_one_add [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (1 + r) :=
  add_comm r 1 ▸ isUnit_add_one hnil

Nilpotent Elements Yield Units via One Plus: $1 + r$ is a unit when $r$ is nilpotent

Informal description

Let $R$ be a ring and $r \in R$ be a nilpotent element. Then $1 + r$ is a unit in $R$.

IsNilpotent.isUnit_add_left_of_commute theorem

[Ring R] {r u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) : IsUnit (u + r)

Full source

theorem IsNilpotent.isUnit_add_left_of_commute [Ring R] {r u : R}
    (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
    IsUnit (u + r) := by
  rw [← Units.isUnit_mul_units _ hu.unit⁻¹, add_mul, IsUnit.mul_val_inv]
  replace h_comm : Commute r (↑hu.unit⁻¹) := Commute.units_inv_right h_comm
  refine IsNilpotent.isUnit_one_add ?_
  exact (hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

Sum of Unit and Commuting Nilpotent is Unit

Informal description

Let $R$ be a ring, and let $r, u \in R$ such that $r$ is nilpotent, $u$ is a unit, and $r$ commutes with $u$. Then the sum $u + r$ is a unit in $R$.

IsNilpotent.isUnit_add_right_of_commute theorem

[Ring R] {r u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) : IsUnit (r + u)

Full source

theorem IsNilpotent.isUnit_add_right_of_commute [Ring R] {r u : R}
    (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
    IsUnit (r + u) :=
  add_comm r u ▸ hnil.isUnit_add_left_of_commute hu h_comm

Sum of Nilpotent and Commuting Unit is Unit

Informal description

Let $R$ be a ring, and let $r, u \in R$ such that $r$ is nilpotent, $u$ is a unit, and $r$ commutes with $u$. Then the sum $r + u$ is a unit in $R$.

IsUnit.not_isNilpotent theorem

[Ring R] [Nontrivial R] {x : R} (hx : IsUnit x) : ¬IsNilpotent x

Full source

lemma IsUnit.not_isNilpotent [Ring R] [Nontrivial R] {x : R} (hx : IsUnit x) :
    ¬ IsNilpotent x := by
  intro H
  simpa using H.isUnit_add_right_of_commute hx.neg (by simp)

Units in Nontrivial Rings are Not Nilpotent

Informal description

Let $R$ be a nontrivial ring. For any unit $x \in R$, $x$ is not nilpotent.

IsNilpotent.not_isUnit theorem

[Ring R] [Nontrivial R] {x : R} (hx : IsNilpotent x) : ¬IsUnit x

Full source

lemma IsNilpotent.not_isUnit [Ring R] [Nontrivial R] {x : R} (hx : IsNilpotent x) :
    ¬ IsUnit x :=
  mt IsUnit.not_isNilpotent (by simpa only [not_not] using hx)

Nilpotent elements in nontrivial rings are not units

Informal description

Let $R$ be a nontrivial ring. For any nilpotent element $x \in R$, $x$ is not a unit.

instIsReducedProd instance

[Zero R] [Pow R ℕ] [Zero S] [Pow S ℕ] [IsReduced R] [IsReduced S] : IsReduced (R × S)

Full source

instance [Zero R] [Pow R ℕ] [Zero S] [Pow S ℕ] [IsReduced R] [IsReduced S] : IsReduced (R × S) where
  eq_zero _ := fun ⟨n, hn⟩ ↦ have hn := Prod.ext_iff.1 hn
    Prod.ext (IsReduced.eq_zero _ ⟨n, hn.1⟩) (IsReduced.eq_zero _ ⟨n, hn.2⟩)

Product of Reduced Structures is Reduced

Informal description

For any reduced structures $(R, 0, \cdot^n)$ and $(S, 0, \cdot^n)$, the product structure $R \times S$ is also reduced.

Prime.isRadical theorem

[CommMonoidWithZero R] {y : R} (hy : Prime y) : IsRadical y

Full source

theorem Prime.isRadical [CommMonoidWithZero R] {y : R} (hy : Prime y) : IsRadical y :=
  fun _ _ ↦ hy.dvd_of_dvd_pow

Primes are Radical in a Commutative Monoid with Zero

Informal description

In a commutative monoid with zero $R$, every prime element $y$ is radical, meaning that for any natural number $n$ and any element $x \in R$, if $y$ divides $x^n$, then $y$ divides $x$.

zero_isRadical_iff theorem

[MonoidWithZero R] : IsRadical (0 : R) ↔ IsReduced R

Full source

theorem zero_isRadical_iff [MonoidWithZero R] : IsRadicalIsRadical (0 : R) ↔ IsReduced R := by
  simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]
  exact forall_swap

Zero is Radical iff Monoid is Reduced

Informal description

For a monoid with zero $R$, the zero element $0$ is radical if and only if $R$ is reduced (i.e., has no nonzero nilpotent elements).

isReduced_iff_pow_one_lt theorem

[MonoidWithZero R] (k : ℕ) (hk : 1 < k) : IsReduced R ↔ ∀ x : R, x ^ k = 0 → x = 0

Full source

theorem isReduced_iff_pow_one_lt [MonoidWithZero R] (k : ℕ) (hk : 1 < k) :
    IsReducedIsReduced R ↔ ∀ x : R, x ^ k = 0 → x = 0 := by
  simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]

Characterization of Reduced Monoids via Powers: $R$ is reduced $\iff$ ($x^k = 0 \implies x = 0$) for all $k > 1$

Informal description

A monoid with zero $R$ is reduced (i.e., has no nonzero nilpotent elements) if and only if for every natural number $k > 1$ and every element $x \in R$, $x^k = 0$ implies $x = 0$.

IsRadical.of_dvd theorem

[CancelCommMonoidWithZero R] {x y : R} (hy : IsRadical y) (h0 : y ≠ 0) (hxy : x ∣ y) : IsRadical x

Full source

theorem IsRadical.of_dvd [CancelCommMonoidWithZero R] {x y : R} (hy : IsRadical y) (h0 : y ≠ 0)
    (hxy : x ∣ y) : IsRadical x := (isRadical_iff_pow_one_lt 2 one_lt_two).2 <| by
  obtain ⟨z, rfl⟩ := hxy
  refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)
  rw [mul_pow, sq z]; exact mul_dvd_mul dvd (dvd_mul_left z z)

Radicality is Preserved by Divisibility in Cancelative Commutative Monoids with Zero

Informal description

Let $R$ be a cancelative commutative monoid with zero. For any nonzero elements $x, y \in R$ such that $y$ is radical and $x$ divides $y$, then $x$ is also radical.

Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero theorem

(h_comm : Commute x y) {m n k : ℕ} (hx : x ^ m = 0) (hy : y ^ n = 0) (h : m + n ≤ k + 1) : (x + y) ^ k = 0

Full source

theorem add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero (h_comm : Commute x y) {m n k : ℕ}
    (hx : x ^ m = 0) (hy : y ^ n = 0) (h : m + n ≤ k + 1) :
    (x + y) ^ k = 0 := by
  rw [h_comm.add_pow']
  apply Finset.sum_eq_zero
  rintro ⟨i, j⟩ hij
  suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero]
  by_cases hi : m ≤ i
  · rw [pow_eq_zero_of_le hi hx, zero_mul]
  rw [pow_eq_zero_of_le ?_ hy, mul_zero]
  linarith [Finset.mem_antidiagonal.mp hij]

Nilpotency of Sum of Commuting Nilpotent Elements with Exponent Bound

Informal description

Let $x$ and $y$ be commuting elements in a semiring such that $x^m = 0$ and $y^n = 0$ for some natural numbers $m, n$. If $m + n \leq k + 1$ for some natural number $k$, then $(x + y)^k = 0$.

Commute.add_pow_add_eq_zero_of_pow_eq_zero theorem

(h_comm : Commute x y) {m n : ℕ} (hx : x ^ m = 0) (hy : y ^ n = 0) : (x + y) ^ (m + n - 1) = 0

Full source

theorem add_pow_add_eq_zero_of_pow_eq_zero (h_comm : Commute x y) {m n : ℕ}
    (hx : x ^ m = 0) (hy : y ^ n = 0) :
    (x + y) ^ (m + n - 1) = 0 :=
  h_comm.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero hx hy <| by rw [← Nat.sub_le_iff_le_add]

Nilpotency of Sum of Commuting Nilpotent Elements with Exponent $m + n - 1$

Informal description

Let $x$ and $y$ be commuting elements in a semiring such that $x^m = 0$ and $y^n = 0$ for some natural numbers $m, n$. Then $(x + y)^{m + n - 1} = 0$.

Commute.isNilpotent_add theorem

(h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent (x + y)

Full source

theorem isNilpotent_add (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
    IsNilpotent (x + y) := by
  obtain ⟨n, hn⟩ := hx
  obtain ⟨m, hm⟩ := hy
  exact ⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩

Nilpotency of Sum of Commuting Nilpotent Elements

Informal description

Let $x$ and $y$ be commuting elements in a semiring. If $x$ and $y$ are nilpotent, then their sum $x + y$ is also nilpotent.

Commute.isNilpotent_sum theorem

 {ι : Type*} {s : Finset ι} {f : ι → R} (hnp : ∀ i ∈ s, IsNilpotent (f i))
  (h_comm : ∀ i j, i ∈ s → j ∈ s → Commute (f i) (f j)) : IsNilpotent (∑ i ∈ s, f i)

Full source

protected lemma isNilpotent_sum {ι : Type*} {s : Finset ι} {f : ι → R}
    (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ i j, i ∈ s → j ∈ s → Commute (f i) (f j)) :
    IsNilpotent (∑ i ∈ s, f i) := by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert j s hj ih => ?_
  rw [Finset.sum_insert hj]
  apply Commute.isNilpotent_add
  · exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
  · apply hnp; simp
  · exact ih (fun i hi ↦ hnp i (by simp [hi]))
      (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))

Nilpotency of Finite Sum of Pairwise Commuting Nilpotent Elements

Informal description

Let $R$ be a semiring, $\iota$ a type, $s$ a finite set of indices from $\iota$, and $f : \iota \to R$ a function. If for every $i \in s$ the element $f(i)$ is nilpotent, and for every $i, j \in s$ the elements $f(i)$ and $f(j)$ commute, then the sum $\sum_{i \in s} f(i)$ is nilpotent.

Commute.isNilpotent_finsum theorem

 {ι : Type*} {f : ι → R} (hf : ∀ b, IsNilpotent (f b)) (h_comm : ∀ i j, Commute (f i) (f j)) : IsNilpotent (finsum f)

Full source

theorem isNilpotent_finsum {ι : Type*} {f : ι → R}
    (hf : ∀ b, IsNilpotent (f b)) (h_comm : ∀ i j, Commute (f i) (f j)) :
    IsNilpotent (finsum f) := by
  classical
  by_cases h : Set.Finite f.support
  · rw [finsum_def, dif_pos h]
    exact Commute.isNilpotent_sum (fun b _ ↦ hf b) (fun _ _ _ _ ↦ h_comm _ _)
  · simp only [finsum_def, dif_neg h, IsNilpotent.zero]

Nilpotency of Sum of Pairwise Commuting Nilpotent Elements over an Index Type

Informal description

Let $R$ be a semiring and $\iota$ a type. Given a function $f : \iota \to R$ such that for every $b \in \iota$, the element $f(b)$ is nilpotent, and for every $i, j \in \iota$, the elements $f(i)$ and $f(j)$ commute, then the sum $\sum_{b \in \iota} f(b)$ (taken over all $b$ where $f(b) \neq 0$) is nilpotent.

Commute.isNilpotent_mul_left_iff theorem

(h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsLeft R) : IsNilpotent (x * y) ↔ IsNilpotent x

Full source

protected lemma isNilpotent_mul_left_iff (h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsLeft R) :
    IsNilpotentIsNilpotent (x * y) ↔ IsNilpotent x := by
  refine ⟨?_, h_comm.isNilpotent_mul_left⟩
  rintro ⟨k, hk⟩
  rw [mul_pow h_comm] at hk
  exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hy k _ hk⟩

Nilpotency of Product with Left Non-Zero Divisor under Commutativity: $xy$ nilpotent $\leftrightarrow$ $x$ nilpotent

Informal description

Let $x$ and $y$ be elements in a ring $R$ such that $x$ and $y$ commute (i.e., $xy = yx$) and $y$ is a left non-zero divisor (i.e., $y \in \text{nonZeroDivisorsLeft}(R)$). Then the product $xy$ is nilpotent if and only if $x$ is nilpotent.

Commute.isNilpotent_mul_right_iff theorem

(h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsRight R) : IsNilpotent (x * y) ↔ IsNilpotent y

Full source

protected lemma isNilpotent_mul_right_iff (h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsRight R) :
    IsNilpotentIsNilpotent (x * y) ↔ IsNilpotent y := by
  refine ⟨?_, h_comm.isNilpotent_mul_right⟩
  rintro ⟨k, hk⟩
  rw [mul_pow h_comm] at hk
  exact ⟨k, (nonZeroDivisorsRight R).pow_mem hx k _ hk⟩

Nilpotency of Product with Right Non-Zero Divisor: $x * y$ nilpotent $\leftrightarrow$ $y$ nilpotent

Informal description

Let $x$ and $y$ be elements in a ring $R$ such that $x$ and $y$ commute (i.e., $x * y = y * x$) and $x$ is a right non-zero divisor (i.e., $x \in \text{nonZeroDivisorsRight}(R)$). Then the product $x * y$ is nilpotent if and only if $y$ is nilpotent.

Commute.isNilpotent_sub theorem

(h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent (x - y)

Full source

theorem isNilpotent_sub (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
    IsNilpotent (x - y) := by
  rw [← neg_right_iff] at h_comm
  rw [← isNilpotent_neg_iff] at hy
  rw [sub_eq_add_neg]
  exact h_comm.isNilpotent_add hx hy

Nilpotency of Difference of Commuting Nilpotent Elements: $x - y$ nilpotent when $x, y$ commute and are nilpotent

Informal description

Let $x$ and $y$ be commuting elements in a ring $R$. If $x$ and $y$ are nilpotent, then their difference $x - y$ is also nilpotent.

isNilpotent_sum theorem

{ι : Type*} {s : Finset ι} {f : ι → R} (hnp : ∀ i ∈ s, IsNilpotent (f i)) : IsNilpotent (∑ i ∈ s, f i)

Full source

lemma isNilpotent_sum {ι : Type*} {s : Finset ι} {f : ι → R}
    (hnp : ∀ i ∈ s, IsNilpotent (f i)) :
    IsNilpotent (∑ i ∈ s, f i) :=
  Commute.isNilpotent_sum hnp fun _ _ _ _ ↦ Commute.all _ _

Nilpotency of Finite Sum of Nilpotent Elements

Informal description

Let $R$ be a semiring, $\iota$ a type, $s$ a finite subset of $\iota$, and $f : \iota \to R$ a function. If for every $i \in s$ the element $f(i)$ is nilpotent, then the sum $\sum_{i \in s} f(i)$ is nilpotent.

isNilpotent_finsum theorem

{ι : Type*} {f : ι → R} (hf : ∀ b, IsNilpotent (f b)) : IsNilpotent (finsum f)

Full source

theorem isNilpotent_finsum {ι : Type*} {f : ι → R}
    (hf : ∀ b, IsNilpotent (f b)) :
    IsNilpotent (finsum f) :=
  Commute.isNilpotent_finsum hf fun _ _ ↦ Commute.all _ _

Nilpotency of Sum of Nilpotent Elements over an Index Type

Informal description

Let $R$ be a semiring and $\iota$ a type. Given a function $f : \iota \to R$ such that for every $b \in \iota$, the element $f(b)$ is nilpotent, then the sum $\sum_{b \in \iota} f(b)$ (taken over all $b$ where $f(b) \neq 0$) is nilpotent.

NoZeroSMulDivisors.isReduced theorem

(R M : Type*) [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] : IsReduced R

Full source

lemma NoZeroSMulDivisors.isReduced (R M : Type*)
    [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] :
    IsReduced R := by
  refine ⟨fun x ⟨k, hk⟩ ↦ ?_⟩
  induction' k with k ih
  · rw [pow_zero] at hk
    exact eq_zero_of_zero_eq_one hk.symm x
  · obtain ⟨m : M, hm : m ≠ 0⟩ := exists_ne (0 : M)
    have : x ^ (k + 1) • m = 0 := by simp only [hk, zero_smul]
    rw [pow_succ', mul_smul] at this
    rcases eq_zero_or_eq_zero_of_smul_eq_zero this with rfl | hx
    · rfl
    · exact ih <| (eq_zero_or_eq_zero_of_smul_eq_zero hx).resolve_right hm

No Zero Smul Divisors Implies Reduced Ring

Informal description

Let $R$ and $M$ be types with the following structures: - $R$ is a monoid with zero, - $M$ has a zero element and a multiplicative action of $R$ with zero, - $M$ is nontrivial (contains at least two distinct elements), - $R$ and $M$ satisfy the no zero smul divisors property (i.e., for any $r \in R$ and $m \in M$, $r \cdot m = 0$ implies $r = 0$ or $m = 0$). Then $R$ is reduced, meaning it has no nonzero nilpotent elements (i.e., for any $x \in R$, if there exists $n \in \mathbb{N}$ such that $x^n = 0$, then $x = 0$).

Main definitions