# Zulip Chat Archive

## Stream: new members

### Topic: zero divisors and nilpotents

#### Aniruddh Agarwal (May 17 2020 at 17:53):

Which definition would be considered better:

```
def is_nilpotent [comm_ring α] (a : α) := ∃ n : ℕ, a ^ n = 0
def is_nilpotent' [comm_ring α] {n : ℕ} (a : α) := a ^ n = 0
```

#### Kevin Buzzard (May 17 2020 at 17:53):

Top one

#### Kevin Buzzard (May 17 2020 at 17:54):

The bottom one would be hard to use because in most cases Lean would not be able to guess `n`

.

#### Patrick Stevens (May 17 2020 at 17:54):

The bottom one would force the user to know the witness to nilpotence, right?

#### Patrick Stevens (May 17 2020 at 17:54):

^^

#### Aniruddh Agarwal (May 17 2020 at 19:10):

I've almost proved that nonzero nilpotents are zero divisors, I just need to prove

```
theorem nonzero_nilpotent_has_nonzero_power [comm_ring α] :
∀ a : α, a ≠ 0 → is_nilpotent a → ∃ m : ℕ, a^m ≠ 0 ∧ ∀ n : ℕ, n > m → a^n = 0
:= sorry
```

to get it, but I'm stumped. I want to find `m`

by taking the minimum of the set (type?) `{ n : ℕ | a^n = 0 }`

, but I'm not sure how to set that up. Here's where I'm at so far:

```
import algebra.associated
import algebra.group_power
variables {α : Type*}
/- An element a of a ring α is a zero divisor if there exists a b ∈ α
such that b ≠ 0 and ab = 0. -/
def is_zero_divisor [comm_ring α] (a : α) := ∃ b : α, b ≠ 0 ∧ a * b = 0
/- An element a of a ring α is nilpotent if there exists a n ∈ ℕ such
that n ≠ 0 and a^n = 0 -/
def is_nilpotent [comm_ring α] (a : α) := ∃ n : ℕ, n ≠ 0 ∧ a ^ n = 0
/- If a is a nonzero nilpotent, then we can find a nonzero natural m
such that a^m ≠ 0 and a^n = 0 for all n > m. -/
theorem nonzero_nilpotent_has_nonzero_power [comm_ring α] :
∀ a : α, a ≠ 0 → is_nilpotent a → ∃ m : ℕ, a^m ≠ 0 ∧ ∀ n : ℕ, n > m → a^n = 0
:=
begin
unfold is_nilpotent,
intros a hanz hanlp,
have set := { n : ℕ | a^n = 0 },
sorry,
end
```

I apparently can't just write `min set`

to get the minimum because lean can't find an instance of a `decidable_linear_order`

for `N`

. Any advice?

#### Bhavik Mehta (May 17 2020 at 19:13):

Try going classical, it might be the decidability that causes issues

#### Aniruddh Agarwal (May 17 2020 at 19:15):

Sorry, can you be more specific?

#### Bhavik Mehta (May 17 2020 at 19:15):

In this specific case though, `nat.find`

is what you probably should use

#### Bhavik Mehta (May 17 2020 at 19:18):

```
begin
classical,
unfold is_nilpotent,
intros a hanz hanlp,
let property : ℕ → Prop := λ n, a^n = 0,
have there_is_some : ∃ n, property n,
sorry,
let m := nat.find there_is_some,
have : a^m = 0 := nat.find_spec there_is_some,
end
```

#### Bhavik Mehta (May 17 2020 at 19:19):

Here's a sketch of how you might use `nat.find`

#### Bhavik Mehta (May 17 2020 at 19:19):

(in your case, the property maybe should be `a^n ≠ 0`

, I haven't checked)

#### Mario Carneiro (May 17 2020 at 19:20):

I guess it could just be the existential in `is_nilpotent`

: `∃ n : ℕ, n ≠ 0 ∧ a ^ n = 0`

#### Bhavik Mehta (May 17 2020 at 19:20):

That could work too

#### Bhavik Mehta (May 17 2020 at 19:21):

@Aniruddh Agarwal, you might also like to note that I used `let`

instead of `have`

sometimes - `have`

doesn't keep track of the actual definition, just its type (so it's the right sort of thing for properties, since we don't care about what the actual proof was) but `let`

does keep track of how it was defined

#### Reid Barton (May 17 2020 at 19:29):

`n ≠ 0`

is unnecessary; is there a reason to include it?

#### Mario Carneiro (May 17 2020 at 19:39):

In this case you probably want to find the least `m`

such that `a^(m+1)=0`

#### Aniruddh Agarwal (May 17 2020 at 20:53):

@Bhavik Mehta I've slightly modified your sketch to get to

```
begin
classical,
unfold is_nilpotent,
intros a hanz hanlp,
have there_is_some : ∃ n, a^(n+1) = 0,
sorry,
have m := nat.find_min' there_is_some,
end
```

which is *almost* what I want, except that `m`

's type

```
m : (λ (n : ℕ), a ^ (n + 1) = 0) ?m_1 → nat.find there_is_some ≤ ?m_1
```

contains a dummy variable `?m_1`

#### Bhavik Mehta (May 17 2020 at 20:55):

The dummy variable represents a natural you haven't chosen yet

#### Bhavik Mehta (May 17 2020 at 20:55):

Once the dummy variable is picked (I'll call it `t`

), `m`

would have type `a^(t + 1) = 0 → nat.find there_is_some ≤ t`

#### Bhavik Mehta (May 17 2020 at 20:58):

Have a look at the functions around `nat.find`

to see what you're given to work with:

```
protected def find : ℕ := nat.find_x.1
protected theorem find_spec : p nat.find := nat.find_x.2.left
protected theorem find_min : ∀ {m : ℕ}, m < nat.find → ¬p m := nat.find_x.2.right
protected theorem find_min' {m : ℕ} (h : p m) : nat.find ≤ m :=
le_of_not_gt (λ l, find_min l h)
```

#### Aniruddh Agarwal (May 17 2020 at 22:11):

I'm still confused and unable to get the minimum of that set out using those functions around `nat.find`

:/

#### Kevin Buzzard (May 17 2020 at 22:15):

Look at the type of `nat.find`

. That tells you what it does. What is your exact problem? Post some working code

#### Aniruddh Agarwal (May 17 2020 at 22:46):

There is where I'm currently stuck:

```
import algebra.associated
import algebra.group_power
variables {α : Type*}
/- An element a of a ring α is nilpotent if there exists a n ∈ ℕ such
that a^n = 0. -/
def is_nilpotent [comm_ring α] (a : α) := ∃ n : ℕ, n ≠ 0 ∧ a ^ n = 0
/- If a is a nonzero nilpotent, then we can find a nonzero natural m
such that a^m ≠ 0 and a^n = 0 for all n > m. -/
theorem nonzero_nilpotent_has_nonzero_power [comm_ring α] :
∀ a : α, a ≠ 0 → is_nilpotent a → ∃ m : ℕ, a^m ≠ 0 ∧ ∀ n : ℕ, n > m → a^n = 0
:=
begin
classical,
unfold is_nilpotent,
intros a hanz hanlp,
have there_is_some : ∃ n, a^(n+1) = 0,
cases hanlp with n hn,
cases n with,
have bad := hn.left,
contradiction,
constructor,
rw nat.succ_eq_add_one at hn,
exact hn.right,
have m := nat.find there_is_some,
have hm := nat.find_min' there_is_some,
constructor,
split,
-- I want to show that m satisfies a^(m+1)=0
sorry,
sorry,
sorry,
sorry,
end
```

#### Kevin Buzzard (May 17 2020 at 22:47):

Can we please change the definition of nilpotent by dropping the n != 0 condition?

#### Kevin Buzzard (May 17 2020 at 22:47):

It just makes things harder

#### Kevin Buzzard (May 17 2020 at 22:49):

oh but then your proof will need refactoring

#### Mario Carneiro (May 17 2020 at 22:50):

You forgot to use `nat.find_spec`

#### Reid Barton (May 17 2020 at 22:51):

Do you need this statement? How about there exists `m`

such that `a^m = 0`

and `a^n \ne 0`

for `n < m`

?

#### Kevin Buzzard (May 17 2020 at 22:52):

Yes what you're doing does look like an unnatural thing to prove

#### Kevin Buzzard (May 17 2020 at 22:53):

`let m := nat.find there_is_some,`

not `have`

#### Kevin Buzzard (May 17 2020 at 22:57):

Reid's suggestion is better because it doesn't involve this unnatural hypothesis about a being non-zero.

#### Kevin Buzzard (May 17 2020 at 22:59):

Why not fix the definition of nilpotent and then prove what Reid suggests?

#### Kevin Buzzard (May 17 2020 at 23:02):

The trick with these things is to find the right statement which doesn't have special cases such as "doesn't work if a=0".

#### Mario Carneiro (May 17 2020 at 23:05):

How about `\exists m, \forall n, a^n = 0 <-> m <= n`

#### Mario Carneiro (May 17 2020 at 23:06):

everything is better with iff

#### Kevin Buzzard (May 17 2020 at 23:07):

```
import algebra.associated
import algebra.group_power
variables {α : Type*}
open_locale classical
/- An element a of a ring α is nilpotent if there exists a n ∈ ℕ such
that a^n = 0. -/
def is_nilpotent [comm_ring α] (a : α) := ∃ n : ℕ, a ^ n = 0
/- If a is a nonzero nilpotent, then we can find a nonzero natural m
such that a^m ≠ 0 and a^n = 0 for all n > m. -/
theorem nonzero_nilpotent_has_nonzero_power [comm_ring α] :
∀ a : α, is_nilpotent a → ∃ m : ℕ, a^m = 0 ∧ ∀ n : ℕ, n < m → a^n ≠ 0
:=
begin
rintros a hna,
use nat.find hna,
split,
{ exact nat.find_spec hna},
{ intro n,
exact nat.find_min hna}
end
```

#### Kevin Buzzard (May 17 2020 at 23:07):

Reid's version comes out really nicely.

#### Kevin Buzzard (May 17 2020 at 23:08):

Mario's version will also come out nicely

#### Reid Barton (May 17 2020 at 23:20):

```
- such that a^m ≠ 0 and a^n = 0 for all n > m. -/
+ such that a^m = 0 and a^n ≠ 0 for all n < m. -/
```

#### Kevin Buzzard (May 18 2020 at 09:49):

@Aniruddh Agarwal here is a way of thinking about all this. You want to find a way of expressing, in Lean, the following idea: if a is nilpotent, and you look at the function from $\mathbb{N}$ to $\{T,F\}$ which sends $n$ to the truth-value of the question "Is $a^n=0$?", then this function looks like "F,F,F,...,F,...,F,T,T,T,...,T,T,...". This is an idea, not a formalised statement. There are lots of different ways to formalise it. You chose one way, which treated the case a=0 as a special case (where the function looks like "T,T,T,T,..." or "F,T,T,T,..." depending on whether R is the zero ring or not) but one could just as well prove the lemma that said that a=0 iff a^n=0 for all n>=1, which would be a much nicer way of dealing with a=0 rather than trying to formalise something general and then leaving out the a=0 case. Leaving in a=0 for now, we want to formalise the idea that there will be 0 or more F's, but a finite number, followed by a bunch of T's. Because 0 F's is possible (if R=0 and a=0) we should let the "key" natural number be the first T, rather than the last F (which might not exist in general). If you are in a situation where you want the index of the last F assuming a isn't zero, you'll be able to get it by subtracting 1 from the first T. But the more natural lemma is the one which applies for all a, rather than just non-zero a.

In short, the lemmas which one wants to formalise are the ones with the most natural statements and the fewest edge cases.

#### Jalex Stark (May 18 2020 at 13:23):

of course the things kevin says about picking natural statements is also true when doing "paper maths", but human mathematicians can elaborate away the "trivial" edge-cases

#### Aniruddh Agarwal (May 18 2020 at 18:42):

:sigh: I finally finished the proof that nonzero nilpotents are zero divisors: https://github.com/anrddh/commutative-algebra-playground/blob/master/src/zero_divisors_and_nilpotents.lean#L45

#### Aniruddh Agarwal (May 18 2020 at 18:45):

Thanks all for your substantial help

#### Kevin Buzzard (May 18 2020 at 18:54):

```
theorem nz_nilpotent_is_zerodivisor [comm_ring α] :
∀ a : α, is_nilpotent a → a ≠ 0 → is_zero_divisor a
:=
begin
rintros a ha ha',
rcases exists_min_pow_zero_of_nilpotent a ha with ⟨m, hm1, hm2⟩,
cases m with m,
{ -- a^0=0 can't happen
exfalso,
apply ha',
apply eq_zero_of_zero_eq_one,
rw ←hm1,
refl
},
{ use a^m,
split,
{ apply hm2,
exact lt_add_one m
},
rw ←hm1,
rw pow_succ
}
end
```

#### Kevin Buzzard (May 18 2020 at 18:55):

You shouldn't really use `simp`

in the middle of proofs, they will break later on as `simp`

gets smarter.

#### Kevin Buzzard (May 18 2020 at 19:02):

```
/- All nonzero nilpotents are zerodivisors. -/
theorem nz_nilpotent_is_zerodivisor [comm_ring α] (a : α) (ha : is_nilpotent a) (ha' : a ≠ 0) : is_zero_divisor a
:=
let ⟨m, hm1, hm2⟩ := exists_min_pow_zero_of_nilpotent a ha in
begin
cases m with m,
{ exact false.elim (ha' (eq_zero_of_zero_eq_one _ hm1.symm _))},-- a^0=0 can't happen
{ exact ⟨a^m, hm2 _ (lt_add_one m), hm1⟩}
end
```

#### Kevin Buzzard (May 18 2020 at 19:06):

I can't figure out how to get the `cases`

into term mode, but if I could this could be a completely term mode proof. The term proof is the same as the tactic proof, each tactic can be turned into a term.

#### Patrick Stevens (May 18 2020 at 19:06):

Note that it's perfectly fine to use `simp`

if you phrase things so that `simp`

is doing something *specific*. For example, `have something : foo, by simp`

is safe: even if `simp`

gets smarter, it's not going to start doing awful things to your proof state, because it's been restricted to this one little fragment of proof.

#### Patrick Stevens (May 18 2020 at 19:08):

(Although for efficiency, mathlib uses `squeeze_simp`

to discover a more minimal subset of things that `simp`

would use, and then restricts the call to `simp`

using `only`

so that it only uses those things)

#### Patrick Stevens (May 18 2020 at 19:16):

Kevin Buzzard said:

I can't figure out how to get the

`cases`

into term mode, but if I could this could be a completely term mode proof. The term proof is the same as the tactic proof, each tactic can be turned into a term.

I'm not sure it's possible, although my confidence here is weak - `exists_min_pow_zero_of_nilpotent`

has output a `Prop`

existential, but to extract anything from this in term mode you'd need a `Type`

, wouldn't you?

#### Kevin Buzzard (May 18 2020 at 19:26):

Patrick Stevens said:

I'm not sure it's possible, although my confidence here is weak -

`exists_min_pow_zero_of_nilpotent`

has output a`Prop`

existential, but to extract anything from this in term mode you'd need a`Type`

, wouldn't you?

I don't know, this is all a bit CS for me.

#### Alex J. Best (May 18 2020 at 19:33):

```
/- All nonzero nilpotents are zerodivisors. -/
theorem nz_nilpotent_is_zerodivisor' [comm_ring α] (a : α) (ha : is_nilpotent a) (ha' : a ≠ 0) : is_zero_divisor a
:= match exists_min_pow_zero_of_nilpotent a ha with
| ⟨0, hm1, hm2⟩ := false.elim (ha' (eq_zero_of_zero_eq_one _ hm1.symm _))
| ⟨(m+1), hm1, hm2⟩ := ⟨a^m, hm2 _ (lt_add_one m), hm1⟩
end
```

terms are love, terms are life

#### Mario Carneiro (May 18 2020 at 20:07):

Patrick Stevens said:

I'm not sure it's possible, although my confidence here is weak -

`exists_min_pow_zero_of_nilpotent`

has output a`Prop`

existential, but to extract anything from this in term mode you'd need a`Type`

, wouldn't you?

`exists_min_pow_zero_of_nilpotent`

can be proven in `Type`

, since it has an explicit witness, namely `nat.find`

of some stuff

Last updated: May 10 2021 at 18:22 UTC