integral domain

Stream: new members

[Damiano Testa]

Dear All,

I am trying to prove that a ring is an integral domain. I can prove that a ring isomorphic to the one that I want is an integral domain (all apparently confirmed by Lean), but I cannot deduce that my initial ring is an integral domain! I realize that I must be missing a very silly command, but I have been unable to find it...

Extra question: after this is done, how can I get Lean to confirm that the ideal by which I divide is prime, since the quotient is an integral domain?

Thank you very much!

import ring_theory.polynomial
import tactic

open polynomial
open ideal

universe u

lemma quoprime {R : Type u} [comm_ring R] (P : ideal R) (H : is_prime P) : integral_domain (quotient (map C P : ideal (polynomial R))) :=
begin
    let quo := polynomial (quotient P),
    let quot := quotient (map C P : ideal (polynomial R)),
    have idq : integral_domain quo, by exact polynomial.integral_domain,
    have iso : quo ≃+* quot, by exact polynomial_quotient_equiv_quotient_polynomial,
        sorry,
end

[Kevin Buzzard]

Can you prove that if R and S are isomorphic rings, and R is an integral domain, then so is S? I think there is a tactic-in-progress to do this, but it is not "true by definition", there's some argument here which is completely mechanical.

[Kevin Buzzard]

As for the other question I guess you need to find a lemma saying R/P is an ID iff P is prime. It will probably be there somewhere...

[Damiano Testa]

I think that I convinced Lean that one of the rings is an integral domain and that the two rings are isomorphic. This is where I am stuck...

[Damiano Testa]

(The code above should also contain a proof of this)

[Kevin Buzzard]

Right. And what I'm saying is that now we need a tactic which rewrites mathematically sane statements along isomorphisms of structures

[Damiano Testa]

I will keep looking for how to transport under isomorphisms

[Damiano Testa]

Ah, I understand what you are saying now...

[Kevin Buzzard]

You could either prove it yourself, or take a look at the current state of the tactic, which I think is called something like equiv_rw

[Damiano Testa]

ok, I will take a look: thanks for the pointer!

[Kevin Buzzard]

Do you know where quotient rings are defined? I've found integral domains but the file makes no mention of quotients.

[Damiano Testa]

I am not sure where quotient rings are defined...

[Kevin Buzzard]

you have them in your file so you can just right click. It's OK, I did it now

[Damiano Testa]

I am still lacking in these basic skills, sorry...

[Kevin Buzzard]

It's in ring_theory.ideal.basic; line 304 is the direction you don't want.

[Damiano Testa]

(sorry, I need to go: I will dig into this later, and will report on what I find!)

[Damiano Testa]

thank you!

[Kevin Buzzard]

import all

example (R : Type) [comm_ring R] (I : ideal R) (hI : integral_domain I.quotient) : I.is_prime :=
begin
  library_search -- fails
end

I don't think it's there!

[Damiano Testa]

More stuff to write!

[Alex J. Best]

docs#ring_equiv.integral_domain is what you want right?

[Kevin Buzzard]

Wow, can I do docs#ring_equiv.discrete_valuation_ring and it just works?

[Kevin Buzzard]

apparently not. So what's the deal here? People just write them if they need them?

[Kevin Buzzard]

docs#ring_equiv.principal_ideal_domain docs#ring_equiv.euclidean_domain docs#ring_equiv.unique_factorization_domain docs#ring_equiv.local_ring

[Kevin Buzzard]

oh man, you just got lucky

[Alex J. Best]

Hahaha well I grepped to find its name first then posted the doc link, but we are all lucky it exists in mathlib already I guess :grinning:

[Kevin Buzzard]

#3951

[Damiano Testa]

That is awesome! Thank you very much @Kevin Buzzard and @Alex J. Best

[Kevin Buzzard]

Note that integral_domain is a Type, and is_integral_domain is a Prop, but the stuff I quote in the PR is the API for converting between them.

[Damiano Testa]

Thanks for the explanation: I am no longer in front of my computer, but will try to use this as soon as I get back!

[Johan Commelin]

docs#ring_equiv.is_integral_domain is more relevant if you already have a ring isomorphism.

[Damiano Testa]

@Johan Commelin Looks like just what I want! Perfect!

[Kevin Buzzard]

Johan: should we have is_field? Is there an issue here with inv?

[Johan Commelin]

Yup, that will quickly lead to defeq issues with inv

[Kevin Buzzard]

Only if people move from is_field to field.

[Johan Commelin]

Which is bound to happen

[Kevin Buzzard]

import tactic

universe u

/-- A predicate to express that a ring is a field.

 This is mainly useful because such a predicate does not contain data,
 and can therefore be easily transported along ring isomorphisms. -/
 structure is_field (R : Type u) [ring R] : Prop :=
(exists_pair_ne : ∃ (x y : R), x ≠ y)
(mul_comm : ∀ (x y : R), x * y = y * x)
(mul_inv_cancel' : ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1)

 /-- Every field satisfies the predicate for integral domains. -/
 lemma field.to_is_field (R : Type u) [field R] :
   is_field R :=
 { mul_inv_cancel' := λ a ha, ⟨a⁻¹, field.mul_inv_cancel ha⟩,
   .. (‹_› : field R) }

open_locale classical

 /-- If a ring satisfies the predicate for integral domains,
 then it can be endowed with an `integral_domain` instance
 whose data is definitionally equal to the existing data. -/
 noncomputable def is_field.to_field (R : Type u) [ring R] (h : is_field R) :
   field R :=
 { inv := λ a, if ha : a = 0 then 0 else classical.some (is_field.mul_inv_cancel' h ha),
   inv_zero := dif_pos rfl,
   mul_inv_cancel := λ a ha,
  begin
    convert classical.some_spec (is_field.mul_inv_cancel' h ha),
    exact dif_neg ha
   end,
   .. (‹_› : ring R), .. (‹_› : is_field R) }

Interested?

[Damiano Testa]

Thank you all again so much! I have laboriously worked through the thread, managed to prove both integral_domain and is_integral_domain, as well as showing that the ideal that I wanted was prime! The subtleties among the presence or absence of is_ are not entirely clear to me, but I can prove both, so that is ok!

Also, I am very happy to now there is a lemma R/P integral domain iff P prime: even though I did not have anything to do with this, I still feel that I am starting to contribute to mathlib! Ahahaha

[Johan Commelin]

@Damiano Testa Do you want an explanation of the subtleties? (It doesn't have real mathematical content, as you probably guessed.)

[Damiano Testa]

Maybe yes, if you have the time, or if you can point me to somewhere where it is already explained...

[Johan Commelin]

@Damiano Testa Do you know the difference between "definitional equality" and "propositional equality"?

[Johan Commelin]

"defeq" means two things are equal by simply unfolding the definitions and nothing else.
Propositional equality means that two things are equal because you can prove it (and maybe even use an axiom, like choice).

[Johan Commelin]

So, in the natural numbers, you can prove n + 0 = n with rfl. Because that is the definition of n + 0.

[Johan Commelin]

On the other hand, 0 + n is defined by induction on n. So to prove 0 + n = n, you need to really do something (namely, repeat the induction on n, and at some point rw along the induction hypothesis.

[Johan Commelin]

So 0 + n = n is only a propositional equality.

[Damiano Testa]

Ok, I have a (probably intuitive) understanding of this: in my mind, it is coded as "defeq : could be an axiom" or "propeq : could be deduced from the axioms"

[Johan Commelin]

Yup, that sounds about right.

[Johan Commelin]

Now why does this matter...

[Damiano Testa]

indeed!

[Johan Commelin]

Lean is trying to help us by automatically finding the semiring structure on nat

[Johan Commelin]

Or the integral domain structure on one of your two rings, etc...

[Johan Commelin]

This is type class inference.

[Johan Commelin]

Now suppose that I am using the addition on nat from mathlib, but you had an addition on nat where you define m + n by induction on m (instead of n, like mathlib does).

[Damiano Testa]

(deleted)

[Johan Commelin]

Oops, you are right. Let me edit it.

[Damiano Testa]

ok, I will erase my comment, then!

[Johan Commelin]

Now you might want to apply the lemma add_comm : m + n = n + m.

[Johan Commelin]

What does this lemma actually say under the hood?

[Damiano Testa]

Johan Commelin said:

This is type class inference.

I had read/heard these words, but not really internalized their meaning

[Johan Commelin]

#print add_comm
theorem add_comm : ∀ {G : Type u} [_inst_1 : add_comm_semigroup G] (a b : G), a + b = b + a :=
λ {G : Type u} [_inst_1 : add_comm_semigroup G], add_comm_semigroup.add_comm

[Johan Commelin]

So lean says, ok, I'll need to find some add_comm_semigroup structure on the natural numbers, and it happily goes away and finds, mine. Out of that, it pulls the definition of addition.

[Johan Commelin]

Let me explain a bit more.

[Johan Commelin]

In a + b, the + is notation for has_add.add

[Johan Commelin]

And lean knows that it can pull has_add.add out of an add_comm_semigroup.

[Johan Commelin]

So, in the end, it will reduce the m + n to nat.add m n.

[Johan Commelin]

However, in your m + n, it had figured out a different nat.add' m n where addition is defined by inducting on m.

[Johan Commelin]

And now it is stuck... because it doesn't know why the two are the same.

[Johan Commelin]

Of course we can prove that they are the same. But Lean can't do so automatically.

[Damiano Testa]

I see: this makes sense also in math! You gave two different definitions of the same additions, but did not prove that they are indeed the same. Is this what is happening?

[Johan Commelin]

So you proofs no longer go smooth, because you will have to remind Lean all the time that two definitions are doing the same thing.

[Johan Commelin]

Damiano Testa said:

I see: this makes sense also in math! You gave two different definitions of the same additions, but did not prove that they are indeed the same. Is this what is happening?

Almost. The trouble is. Even if we prove a lemma

lemma add_eq_add' : nat.add m n = nat.add' m n

we would still need to mention this lemma all the time.

[Johan Commelin]

Whereas in maths, once you prove it, you can forget about it.

[Damiano Testa]

This is starting to become clearer. And it is also clear that I need to understand more about how things are defined in Lean in order to avoid such traps...

[Johan Commelin]

The two defintions will merge into one thing.

[Johan Commelin]

There is actually one really painful occurence of this issue in mathlib/Lean.

[Johan Commelin]

The definition of nat.pow is not defeq to powers in arbitrary monoids.

[Johan Commelin]

(But you don't see this in the notation.)

[Damiano Testa]

Ah, the slogan that I heard from Kevin = is not an equivalence relation in Lean surfaces in my mind

[Johan Commelin]

So we have to rewrite with nat.pow_eq_pow. (And you have to guess in which direction :scream:)

[Johan Commelin]

This is something that we have to fix. But nobody has gone through the trouble so far.

[Johan Commelin]

There are actually other instances as well. $\mathbb{Z}$ is a module over itself in two different ways.

[Johan Commelin]

1. every abelian group is a module over int.
2. every ring is a module over itself.

[Damiano Testa]

Ok, it helps a lot to understand the separation between mathematical issues and computer issues. I feel that I am quite comfortable with the mathematical ones, that the computer ones have "mirrors" in maths, but I am not yet able to see through the mirror

[Johan Commelin]

Currently these two are not defeq. Which causes pain.

[Johan Commelin]

It would help a lot if we could teach lean: "hey, all module instances of anything over int are always propositionally equal. Just use this fact an move on."

[Damiano Testa]

Ok, so is this where the trouble with is_integral_domain and integral_domain begins? That they are not defeq?

[Johan Commelin]

But currently we don't have a way to teach Lean such a fact.

[Johan Commelin]

Damiano Testa said:

Ok, so is this where the trouble with is_integral_domain and integral_domain begins? That they are not defeq?

Not really.

[Johan Commelin]

So let me try to explain that.

[Damiano Testa]

ok, thanks!

[Johan Commelin]

Here is one very important fact: in Lean (but not in all other systems) we have proof irrelevance.

[Damiano Testa]

Yes, I read about this and I am not sure where my (mathematical) stance is on this one!

[Damiano Testa]

But I accept it! Ahahaa

[Johan Commelin]

That means that if P : Prop, and h1 and h2 are proofs of P. In other words h1 : P and h2 : P. Then h1 and h2 are defeq.

[Johan Commelin]

This is baked into Lean core.

[Damiano Testa]

Ok, now I can also follow with the defeq definition from before! This is great! :)

[Johan Commelin]

Yes, and it means that if we have a definition that depends on a proof of P. (Say fin n, which consists of i : nat and h : i < n)

[Johan Commelin]

Then (i, h1) is defeq to (i, h2).

[Johan Commelin]

So we don't care how to prove i < n.

[Johan Commelin]

Now, is_integral_domain R : Prop, because it assumes [comm_ring R] under the hood as an argument.

[Johan Commelin]

So it doesn't matter how you prove is_integral_domain R, all of them are the same to Lean.

[Johan Commelin]

But integral_domain R records all the data, because it extends has_add and has_mul, etc...

[Johan Commelin]

So, in your setup, you has A and B, and both of them already had a comm_ring instance.

[Johan Commelin]

So Lean already knew about has_add A and has_add B.

[Johan Commelin]

So now, what you really don't want to do, is transfer has_add B along an equivalence to obtain a new version of has_add A.

[Johan Commelin]

Because then, all of a sudden, there are two. And they are only propositionally equal.

[Damiano Testa]

This would be a (dire) consequence of using is_integral_domain as opposed to integral_domain, right?

[Johan Commelin]

So, when you extend comm_ring A to integral_domain A, you need to make sure that all the data fields are defeq to what you had. But for the fields that are props, it doesn't matter what you do.

[Johan Commelin]

So transferring is_integral_domain is harmless.

[Johan Commelin]

But transferring integral_domain can be dangerous.

[Damiano Testa]

Ah, I got it mixed up...

[Damiano Testa]

I need to think this through more carefully, then

[Kenny Lau]

this is all theoretical

[Kenny Lau]

you'll internalize it once you run into errors

[Damiano Testa]

I am a little puzzled about this has_add not remembering the proof. I could put two ring structures on a set with 4 elements: Z/4 and (Z/2)^2. If Lean forgets how I proved that there was an addition, how will it know which addition to use?

[Kenny Lau]

has_add is data

[Kenny Lau]

I don't understand what you mean by not remembering the proof

[Kenny Lau]

proof irrelevance only concerns propositions not data

[Damiano Testa]

I was trying to contrast this with

said:

So now, what you really don't want to do, is transfer has_add B along an equivalence to obtain a new version of has_add A.

[Damiano Testa]

For the moment, I have been able to prove both results integral_domain R and is_integral_domain R, so I am happy. The discussion here has helped clarify a lot of hazy stuff, but I still need time to process these concepts. Thank you all for your time and help!

[Reid Barton]

has_add is data, not a proof, so proof irrelevance doesn't apply to it. We don't say things like "I proved that there was an addition" (it's imprecise at best even in ordinary mathematics).

[Reid Barton]

Damiano Testa said:

Yes, I read about this and I am not sure where my (mathematical) stance is on this one!

This might be because you are identifying some things as proofs that Lean doesn't consider to be proofs.

[Damiano Testa]

Ah, so this is precisely the reason why the addition is carried along an equivalence and might cause problems on the other side?

[Damiano Testa]

It is carried along, because it contains actual instructions on how to perform the addition that have nothing to do with proving stuff about it. Maybe I am understanding what is going on

[Damiano Testa]

I think that I see my mistake: when I read that has_add was passed along an equivalence, I thought that Lean simply remembered that there was an addition on one of the two sides. However, if I understand correctly, Lean remembers exactly how to perform the addition and now has two well-defined additions on the same type and can be stuck. Hopefully this is correct!

[Johan Commelin]

Damiano Testa said:

Ah, so this is precisely the reason why the addition is carried along an equivalence and might cause problems on the other side?

Right!

[Johan Commelin]

You want to transfer the proof that addition is commutative. But not the defintion of addition itself.

[Reid Barton]

I don't really know what the context was, but:

• Even in ordinary math, you could certainly define $+$ on something in two different ways. Generally we try to pick just one way because otherwise things would get confusing quickly.
• In Lean, if we have two definitions of $+$ on something, it's not sufficient that they be merely equal by a theorem, because Lean doesn't just know this theorem. You really want them to be the same by definiiton.

[Damiano Testa]

Ok, I am getting the hang of this: thank you so much!

[Kevin Buzzard]

Johan Commelin said:

It would help a lot if we could teach lean: "hey, all module instances of anything over int are always propositionally equal. Just use this fact an move on."

import tactic
import algebra.module.basic

example (M : Type) [add_comm_group M] : subsingleton (module ℤ M) := by apply_instance

[Johan Commelin]

@Kevin Buzzard Sure, but that's not enough

[Johan Commelin]

Because Lean doesn't use that fact when it hits a wall

[Johan Commelin]

And of course there is the other problem that has_scalar Z M is not a subsingleton... so if it hits two different has_scalar instances then there's a nastier issue