Zulip Chat Archive

Stream: new members

Topic: zero divisors and nilpotents


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:53):

Top one

view this post on Zulip 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.

view this post on Zulip Patrick Stevens (May 17 2020 at 17:54):

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

view this post on Zulip Patrick Stevens (May 17 2020 at 17:54):

^^

view this post on Zulip 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?

view this post on Zulip Bhavik Mehta (May 17 2020 at 19:13):

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

view this post on Zulip Aniruddh Agarwal (May 17 2020 at 19:15):

Sorry, can you be more specific?

view this post on Zulip Bhavik Mehta (May 17 2020 at 19:15):

In this specific case though, nat.find is what you probably should use

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 17 2020 at 19:19):

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

view this post on Zulip Bhavik Mehta (May 17 2020 at 19:19):

(in your case, the property maybe should be a^n ≠ 0, I haven't checked)

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 17 2020 at 19:20):

That could work too

view this post on Zulip 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

view this post on Zulip Reid Barton (May 17 2020 at 19:29):

n ≠ 0 is unnecessary; is there a reason to include it?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 17 2020 at 20:55):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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 :/

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:47):

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

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:47):

It just makes things harder

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:49):

oh but then your proof will need refactoring

view this post on Zulip Mario Carneiro (May 17 2020 at 22:50):

You forgot to use nat.find_spec

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:52):

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

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:53):

let m := nat.find there_is_some, not have

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:59):

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

view this post on Zulip 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".

view this post on Zulip Mario Carneiro (May 17 2020 at 23:05):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 23:06):

everything is better with iff

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 17 2020 at 23:07):

Reid's version comes out really nicely.

view this post on Zulip Kevin Buzzard (May 17 2020 at 23:08):

Mario's version will also come out nicely

view this post on Zulip 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. -/

view this post on Zulip 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 N\mathbb{N} to {T,F}\{T,F\} which sends nn to the truth-value of the question "Is an=0a^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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Aniruddh Agarwal (May 18 2020 at 18:45):

Thanks all for your substantial help

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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