Coerce ring ideal to field ideal

Stream: general

[Arnoud van der Leer]

Hi there, it's me again. I am trying to complete the following proof. It should follow easily from mathlib, but apparently I am trying to prove something for an ideal of [ring R] while I have a hypothesis that says something about an ideal of [ring R upgraded to a field]. What am I missing?

lemma p2 {R: Type u} [comm_ring R] : is_field R → ∀ (I: ideal R), I = ⊥ ∨ I = ⊤ :=
begin
  intros h,
  have F := is_field.to_field R h,
  have h2 := @ideal.eq_bot_or_top R F,
  assumption,
end

[Hanting Zhang]

It's docs#ideal.eq_bot_or_top

[Arnoud van der Leer]

Have you looked at the code?

[Hanting Zhang]

Argh, sorry, that was really bad of me. I see the problem now

[Johan Commelin]

@Arnoud van der Leer I'm afraid you need to reprove the eq_bot_or_top lemma.

[Johan Commelin]

Oh, did you try convert h2?

[Kevin Buzzard]

@Arnoud van der Leer can you post a #mwe? I cut and pasted your code but there were errors and I'm too lazy to fix them.

[Arnoud van der Leer]

@Johan Commelin
But if I have to reprove such a simple theorem, does that mean that every theorem about (R: Type u) [field R] will have to reproved for (R: Type u) [comm_ring R] (h: is_field R) and vice versa?

[Kevin Buzzard]

And is there a good reason you're using is_field instead of [field R]? This seems to be what's causing your problem, and I don't see any logical reason for doing it.

[Kevin Buzzard]

Yes maybe, and the moral is that you shouldn't be stating theorems like this at all I guess?

[Arnoud van der Leer]

convert h2 changes the goal to (∀ (I : ideal R), I = ⊥ ∨ I = ⊤) = ∀ (I : ideal R), I = ⊥ ∨ I = ⊤.

[Johan Commelin]

@Arnoud van der Leer is_field is a little bit of glue but isn't idiomatic.

[Johan Commelin]

So you should avoid it, whenever possible.

[Arnoud van der Leer]

@Kevin Buzzard
Oh, sorry, forgot the imports and universes

import ring_theory.ideal.basic
import algebra.field

universes u v

lemma p2 {R: Type u} [comm_ring R] : is_field R → ∀ (I: ideal R), I = ⊥ ∨ I = ⊤ :=
begin
  intros h,
  have F := is_field.to_field R h,
  have h2 := @ideal.eq_bot_or_top R F,
  convert h2,
  assumption,
end

[Kevin Buzzard]

lemma p2 {R: Type u} [comm_ring R] : is_field R → ∀ (I: ideal R), I = ⊥ ∨ I = ⊤ :=
begin
  intros h,
  let F := is_field.to_field R h,
  have h2 := @ideal.eq_bot_or_top R F,
  convert h2,
end

[Kevin Buzzard]

Your problem was that F is data, so needs to be defined with let and not have.

[Arnoud van der Leer]

The is_field was because this is supposed to be part of a three-way equivalence (is there a nice way to prase this, by the way, or should I just make this two equivalences?) between

• R is a field
• R has only two ideals
• Any morphism from R into a nonzero ring is injective
  And I thought if I took is_field instead of field, I would need to prove less for the other implications.

[Arnoud van der Leer]

Kevin Buzzard said:

Your problem was that F is data, so needs to be defined with let and not have.

Oooooh. Thank you!

[Kevin Buzzard]

import ring_theory.ideal.basic
import algebra.field

universes u v

lemma p2 {R: Type u} [comm_ring R] : is_field R → ∀ (I: ideal R), I = ⊥ ∨ I = ⊤ :=
begin
  intros h,
  letI := is_field.to_field R h,
  apply ideal.eq_bot_or_top,
end

Your approach is unidiomatic so we have to jump through some hoops. letI puts the field instance into the type class inference system, and now everything works as normal (you don't need the @)

[Kevin Buzzard]

Your explanation for why you're using is_field is convincing, and is indeed the reason why is_field is there. So you will have to learn to jump through the hoops :-) but that's what we're here for.

[Kevin Buzzard]

One of the differences between field and is_field is that is_field lives in the Prop universe, and field lives in the Type universe (because there is more data in field than ring due to a design decision; the inverse is an explicit input to a field structure).

[Kevin Buzzard]

Another difference is that is_field is a structure but field is a class, so you will have to know something about how type class inference works. The typeclass system is a big database which keeps track of which things are groups, which things are rings etc. Normally you can just leave it alone, feed it with [] stuff at the beginning of your lemmas and defs, and it works fine -- you don't need to add to the database in the middle of a proof. But here what's happening is that half way through the proof you want to add something new to it because of the nature of what you're doing, and that's when letI and haveI come in handy because they enable you to do this.

[Kevin Buzzard]

There's no simple way to prove A <-> B <-> C in Lean without breaking it into two iff's, as far as I know. I think I've covered all your questions now :-)

[Adam Topaz]

Kevin Buzzard said:

There's no simple way to prove A <-> B <-> C in Lean without breaking it into two iff's, as far as I know. I think I've covered all your questions now :-)

There's a tfae tactic, but I've never used it...

[Johan Commelin]

This is a perfect opportunity to use tfae

[Bryan Gin-ge Chen]

We have a few tfae statements here and there in mathlib, but in my opinion they're a bit awkward to use because they require you to refer to numerical labels. See #3532 for a related feature request.

[Kevin Buzzard]

It's not a tactic, and I don't know the API for it :-)

import tactic

example (P Q R : Prop) (hPQ : P ↔ Q) (hQR : Q ↔ R) :
  tfae [P, Q, R] :=
begin
  simp [hPQ, hQR],
  -- ⊢ [R, R, R].tfae
end

[Bryan Gin-ge Chen]

You're right, though the related tactic docs are under tactic#tfae .

[Kevin Buzzard]

import tactic

open list

example (P Q R : Prop) (hPQ : P ↔ Q) (hQR : Q ↔ R) :
  tfae [P, Q, R] :=
begin
  simp [hPQ, hQR, tfae_cons_of_mem, tfae_nil],
  -- ⊢ [R, R, R].tfae -- aargh
  sorry
end

lol

[Bryan Gin-ge Chen]

You just have to say the magic word at the end:

import tactic

example (P Q R : Prop) (hPQ : P ↔ Q) (hQR : Q ↔ R) :
  tfae [P, Q, R] :=
begin
  simp [hPQ, hQR],
  tfae_finish,
end

[Kevin Buzzard]

example (P Q R : Prop) (hPQ : P ↔ Q) (hQR : Q ↔ R) :
  tfae [P, Q, R] :=
begin
  tfae_finish,
end

[Johan Commelin]

@Kevin Buzzard you want things like: tfae_have : 3 → 1,

[Kevin Buzzard]

Yes, I saw the docs now from Bryan's post.

[Arnoud van der Leer]

Kevin Buzzard said:

Another difference is that is_field is a structure but field is a class, so you will have to know something about how type class inference works. The typeclass system is a big database which keeps track of which things are groups, which things are rings etc. Normally you can just leave it alone, feed it with [] stuff at the beginning of your lemmas and defs, and it works fine -- you don't need to add to the database in the middle of a proof. But here what's happening is that half way through the proof you want to add something new to it because of the nature of what you're doing, and that's when letI and haveI come in handy because they enable you to do this.

Thanks a lot for your explanations!