## 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


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?

^^

#### 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,
constructor,
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,
},
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