zero divisors and nilpotents

Stream: new members

[Aniruddh Agarwal]

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]

Top one

[Kevin Buzzard]

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

[Patrick Stevens]

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

[Patrick Stevens]

^^

[Aniruddh Agarwal]

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]

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

[Aniruddh Agarwal]

Sorry, can you be more specific?

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Mario Carneiro]

I guess it could just be the existential in is_nilpotent: ∃ n : ℕ, n ≠ 0 ∧ a ^ n = 0

[Bhavik Mehta]

That could work too

[Bhavik Mehta]

@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]

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

[Mario Carneiro]

In this case you probably want to find the least m such that a^(m+1)=0

[Aniruddh Agarwal]

@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]

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

[Bhavik Mehta]

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]

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]

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

[Kevin Buzzard]

Look at the type of nat.find. That tells you what it does. What is your exact problem? Post some working code

[Aniruddh Agarwal]

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]

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

[Kevin Buzzard]

It just makes things harder

[Kevin Buzzard]

oh but then your proof will need refactoring

[Mario Carneiro]

You forgot to use nat.find_spec

[Reid Barton]

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]

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

[Kevin Buzzard]

let m := nat.find there_is_some, not have

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

everything is better with iff

[Kevin Buzzard]

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]

Reid's version comes out really nicely.

[Kevin Buzzard]

Mario's version will also come out nicely

[Reid Barton]

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

@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]

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]

: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]

Thanks all for your substantial help

[Kevin Buzzard]

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]

You shouldn't really use simp in the middle of proofs, they will break later on as simp gets smarter.

[Kevin Buzzard]

/- 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]

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]

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]

(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]

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]

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]

/- 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]

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