A ring is reduced if 0 has no nonzero square roots

Stream: Is there code for X?

[Artie Khovanov]

Pretty basic lemma, can't find it anywhere, am I duplicating a well-hidden argument?

[Artie Khovanov]

theorem IsReduced.of_sq_eq_zero_imp_eq_zero {R : Type*} [Semiring R]
    (h : ∀ a : R, a ^ 2 = 0 → a = 0) : IsReduced R where
  eq_zero x nx := by
    have ind : ∀ {k}, x ^ (2 ^ k) = 0 → x = 0 := fun {k} hk ↦ by
      induction k with
      | zero => simp_all
      | succ k ih =>
      rw [Nat.pow_succ', mul_comm, pow_mul] at hk
      exact ih (h _ hk)
    rcases nx with ⟨n, hx⟩
    exact ind <| pow_eq_zero_of_le Nat.lt_two_pow_self.le hx

[Violeta Hernández]

docs#IsReduced

[Violeta Hernández]

Surely 2 in this argument generalizes to any natural n > 1?

[Violeta Hernández]

Also, this seems like a version of docs#isReduced_of_noZeroDivisors with weaker hypotheses, so I think you should add it and reprove the noZeroDivisors version using it.

[Artie Khovanov]

Do you mean 2 in the statement or in the proof? In the proof yes, and you can use strong induction on $n$ as well. In the statement no, it becomes false right? Let me think of an example.

[Violeta Hernández]

import Mathlib.Algebra.GroupWithZero.Basic
import Mathlib.Algebra.Ring.Nat
import Mathlib.Order.Basic

theorem IsReduced.of_sq_eq_zero_imp_eq_zero {R : Type*} [Semiring R]
    {n : ℕ} (hn : 1 < n) (h : ∀ a : R, a ^ n = 0 → a = 0) : IsReduced R where
  eq_zero x nx := by
    have ind : ∀ {k}, x ^ (n ^ k) = 0 → x = 0 := fun {k} hk ↦ by
      induction k with
      | zero => simp_all
      | succ k ih =>
      rw [Nat.pow_succ', mul_comm, pow_mul] at hk
      exact ih (h _ hk)
    rcases nx with ⟨n, hx⟩
    exact ind <| pow_eq_zero_of_le (Nat.lt_pow_self hn).le hx

[Artie Khovanov]

Oh lol fair thx

[Artie Khovanov]

I shouldn't think about maths at stupid o clock

[Jakub Nowak]

Technically it's not generalized because it's implied by the version with 2:

import Mathlib

theorem IsReduced.of_sq_eq_zero_imp_eq_zero {R : Type*} [Semiring R]
    (h : ∀ a : R, a ^ 2 = 0 → a = 0) : IsReduced R where
  eq_zero x nx := by
    have ind : ∀ {k}, x ^ (2 ^ k) = 0 → x = 0 := fun {k} hk ↦ by
      induction k with
      | zero => simp_all
      | succ k ih =>
      rw [Nat.pow_succ', mul_comm, pow_mul] at hk
      exact ih (h _ hk)
    rcases nx with ⟨n, hx⟩
    exact ind <| pow_eq_zero_of_le Nat.lt_two_pow_self.le hx

theorem IsReduced.of_pow_eq_zero_imp_eq_zero {R : Type*} [Semiring R]
    (h : ∀ a : R, ∃ n > 1, a ^ n = 0 → a = 0) : IsReduced R :=
  .of_sq_eq_zero_imp_eq_zero fun a h2 ↦ by
    choose n hn h using h a
    apply h
    exact pow_eq_zero_of_le hn h2

theorem IsReduced.of_pow_n_eq_zero_imp_eq_zero {R : Type*} [Semiring R]
    {n : ℕ} (hn : 1 < n) (h : ∀ a : R, a ^ n = 0 → a = 0) : IsReduced R :=
  .of_pow_eq_zero_imp_eq_zero fun a ↦ ⟨n, ⟨hn, h a⟩⟩

Basically, a^2 = 0 is the strongest, because it just implies a^n = 0 for any n > 1.

[Violeta Hernández]

Sure, but changing 2 to n is such a trivial change that we might as well do it anyways.

[Jakub Nowak]

I'm not sure if it is any useful though.

[Riccardo Brasca]

I am not sure, but note that having r ^ 2 = 0 is not enough for grind to conclude that r ^ 3 = 0, so maybe we want the general version.

[Jakub Nowak]

Should we add docs#pow_eq_zero_of_le to grind?

[Riccardo Brasca]

I don't know, I am not familiar enough with grind annotations.

[Artie Khovanov]

Violeta Hernández said:

this seems like a version of docs#isReduced_of_noZeroDivisors with weaker hypotheses

I don't understand. The ring Z[X]/(XY) is reduced and therefore satisfies the hypothesis for all n>1, but X is a zero divisor.

[Junyan Xu]

isReduced_iff_pow_one_lt is already there (assuming MonoidWithZero is enough)
(turns out it was added by me in mathlib3#17002)

[Artie Khovanov]

Junyan Xu said:

isReduced_iff_pow_one_lt is already there (assuming MonoidWithZero is enough)
(turns out it was added by me in mathlib3#17002)

Nice, thanks! Honestly don't know how I thought it didn't generalise. Think I had a sign wrong in my head.

[Artie Khovanov]

Following the proof back, the general induction principle is docs#Nat.pow_imp_self_of_one_lt

[Artie Khovanov]

Mathlib is cool!

[Jakub Nowak]

Do you think this would be useful to add to mathlib? It lets you "come up" with n after you get element a:

theorem IsReduced.of_pow_eq_zero_imp_eq_zero [Monoid R]
    (h : ∀ a : R, ∃ n > 1, a ^ n = 0 → a = 0) : IsReduced R

[Artie Khovanov]

This is just a logically vacuous restatement of the definition, right?

[Jakub Nowak]

I don't think so. You're thinking about ∀ a : R, (∃ n > 1, a ^ n = 0) → a = 0. It's not the same as ∀ a : R, ∃ n > 1, a ^ n = 0 → a = 0, which is parsed as ∀ a : R, ∃ n > 1, (a ^ n = 0 → a = 0).

[Jakub Nowak]

This is kinda a stronger version of {n : ℕ} (hn : 1 < n) (h : ∀ a : R, a ^ n = 0 → a = 0). In the latter you have to pick n and then prove a ^ n = 0 → a = 0 for every a.

With ∀ a : R, ∃ n > 1, a ^ n = 0 → a = 0, for every a you pick n and then prove a ^ n = 0 → a = 0. You can pick a different n for different as.

[Jakub Nowak]

From API perspective this is just a shorthand combination of IsReduced.of_sq_eq_zero_imp_eq_zero and pow_eq_zero_of_le.

[Artie Khovanov]

Oh yep, you're right - this is better, we should add it

[Jakub Nowak]

I'm not so sure about adding it tbh. This lemma is just combination of two different lemmas and it looks hard to find with loogle or existing interactive tactics I'm aware of.