Zulip Chat Archive

Stream: maths

Topic: getting a ring from an integral domain


view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:43):

If I understand correctly the definition

@[protect_proj, ancestor comm_ring domain]
class integral_domain (α : Type u) extends comm_ring α, domain α

of an integral domain, it is something which extends both commutative rings and domains. These two classes both extend rings.

As far as I understand, constructing an "extension" automatically produces maps from comm_ring to ring and from domain to ring allowing to look at a comm_ring (resp. at a domain) as being a ring. Hence there are a priori two maps taking an integral_domain and producing a ring, according to which path one chooses between integral_domain -> domain -> ring and integral_domain -> comm_ring -> ring. Is it clear that the two results coincide?

I am asking because I had a nice proof working for commutative rings, and tried to add the assumption hR : integral_domain R in order to strengthen the result. Now the proof does not compile anymore, giving a bunch of coercion issues, like

invalid type ascription, term has type
  @has_mem.mem R (@ideal R _inst_1)
    (@submodule.has_mem R R (@ring.to_semiring R (@comm_ring.to_ring R _inst_1))
       (@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_1)))
       (@semiring.to_semimodule R (@ring.to_semiring R (@comm_ring.to_ring R _inst_1))))
    (@has_mul.mul R (@distrib.to_has_mul R (@ring.to_distrib R (@comm_ring.to_ring R _inst_1))) x y)
    M
but is expected to have type
  @has_mem.mem R (@ideal R _inst_1)
    (@submodule.has_mem R R (@ring.to_semiring R (@comm_ring.to_ring R _inst_1))
       (@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R (@comm_ring.to_ring R _inst_1)))
       (@semiring.to_semimodule R (@ring.to_semiring R (@comm_ring.to_ring R _inst_1))))
    (@has_mul.mul R (@distrib.to_has_mul R (@ring.to_distrib R (@domain.to_ring R (@integral_domain.to_domain R hR)))) x
       y)
    M

(the last lines are different: one is

@distrib.to_has_mul R (@ring.to_distrib R (@comm_ring.to_ring R _inst_1)))

and the other is

@distrib.to_has_mul R (@ring.to_distrib R (@domain.to_ring R (@integral_domain.to_domain R hR)))

view this post on Zulip Adam Topaz (Nov 13 2020 at 14:52):

Could it be that you have two instances of a commutative ring around? One coming from comm_ring and one from integral_domain?

view this post on Zulip Adam Topaz (Nov 13 2020 at 14:53):

Namely, having both [comm_ring A] and [integral_domain A] would cause issues

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:53):

Oh yes!

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:53):

Thank you so much! I now realize the problem.

view this post on Zulip Adam Topaz (Nov 13 2020 at 14:53):

No problem :)

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:53):

Is there a statement is_integral_domain : ring --> Prop?

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:54):

So that I can add hR : is_integral_domain R?

view this post on Zulip Adam Topaz (Nov 13 2020 at 14:54):

I'm not sure.

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:54):

I wrote hR : integral_domain R and now you make me realize that I have created a second ring called hR to which I asked to be an int. domain...

view this post on Zulip Adam Topaz (Nov 13 2020 at 14:55):

Do you really want to say that the integral domain assumption is a separate assumption?

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:55):

Well, that was my idea because in the applications I had in mind I would expect someone to prove that a ring was an int. domain and then give the proof to the lemma

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 14:56):

But I can add it in the variables definition.

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 15:10):

Adam Topaz said:

Do you really want to say that the integral domain assumption is a separate assumption?

Thanks, it works and the problem was indeed my stupid syntax. At any rate, is the answer to my original question about "the two paths leading to the same result" yes?

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:17):

I think so.

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:17):

You can check... (I'll sketch some code)

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:21):

Here's a roundabout sanity check :rofl:

import algebra

variables (A : Type*) (h : integral_domain A)

include h

def foo1 : comm_ring A := by letI := h; apply_instance
def foo2 : domain A := by letI := h; apply_instance

def foo3 : ring A := by letI := foo1; apply_instance
def foo4 : ring A := by letI := foo2; apply_instance

example : foo3 = foo4 := rfl

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 15:22):

Very nice!

view this post on Zulip Johan Commelin (Nov 13 2020 at 15:31):

is_integral_domain exists.

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 15:32):

Thanks!

view this post on Zulip Kevin Buzzard (Nov 13 2020 at 17:00):

This is somehow a big mess, it trips up a lot of beginners and in some sense I'm not sure we have a good solution for it all yet.

view this post on Zulip Adam Topaz (Nov 13 2020 at 17:27):

I really think the [[...]] idea could be a solution to this issue.

view this post on Zulip Adam Topaz (Nov 13 2020 at 17:29):

In this case, all Prop's defining the axioms for an integral domain would be individual Prop-valued classes (or mixins?, whatever you want to call it), And the "ring" class could just be the data associated with the ring, e.g.

class raw_ring (A : Type*) :=
(zero : A)
(one : A)
(add : A  A  A)
(neg : A  A)
(mul : A  A)

And to declare an integral domain you would just write [[integral_domain A]] and lean should automatically add all the data + mixins as assumptions

view this post on Zulip Adam Topaz (Nov 13 2020 at 17:31):

And this way we also wouldn't have to worry about whether PID and/or DVR should be a prop-valued class assuming integral_domain or something which extends integral_domain.

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:04):

I have no idea what amount of work would be needed to get [[...]] working, but it would be awesome if it works!

view this post on Zulip Eric Wieser (Nov 13 2020 at 18:29):

How should lean handle [[foo A]] [[bar A]] if foo requires [monoid_with_zero A] and bar requires [add_monoid A]? It seems it need to be at least aware enough of diamonds (in this case, to has_zero) to reject them

view this post on Zulip Eric Wieser (Nov 13 2020 at 18:31):

Or maybe if we use [[]] widely enough all the diamonds vanish

view this post on Zulip Bryan Gin-ge Chen (Nov 13 2020 at 18:36):

I'm not in any place to make [[]] happen, but if it's something we really want (for Lean 4?), we should write up an issue somewhere (mathlib? community Lean?), since proposals in Zulip are too easily forgotten.

view this post on Zulip Adam Topaz (Nov 13 2020 at 18:38):

@Eric Wieser You would need a class like [raw_semiring A] for the data of addition, multiplication, zero, and one

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:39):

there is an issue for this

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:40):

leanprover/lean#1522

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:40):

@Adam Topaz Why do we want raw_ring. Can't [[ring A]] just be shorthand for
[has_zero A] .. [has_mul A] [ring_axioms A]?

view this post on Zulip Adam Topaz (Nov 13 2020 at 18:41):

Yeah, I guess you're right @Johan Commelin

view this post on Zulip Adam Topaz (Nov 13 2020 at 18:41):

Except [ring_axioms A] should be [[ring_axioms A]] :)

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:41):

@Johan Commelin Coq has this. It leads to some big performance problems

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:42):

Why?

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:42):

There would always be a direct path to has_add A, which seems a big win to me.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:43):

https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:43):

The TC-graph would only be about inferring comm_ring from principal_ideal_domain and things like that. Just a bunch of props

view this post on Zulip Eric Wieser (Nov 13 2020 at 18:43):

Right - all the to_has_add parts of typeclass search would vanish

view this post on Zulip Mario Carneiro (Nov 13 2020 at 18:44):

the problem is that even ignoring the search itself, the result grows exponentially with the depth of the hierarchy

view this post on Zulip Johan Commelin (Nov 13 2020 at 18:48):

Hmm, I'll have to read that blog (again)

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:06):

@Mario Carneiro From that blogpost:

Taking the superclasses as indices instead of embedding them as fields simplifies typeclass search and is necessary to support diamonds in the hierarchy; see the original paper for more details.

I propose to only index on data-carrying classes like has_one A and has_add A, but not on Props like is_semigroup A or is_comm_ring A.

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:07):

In Lean that doesn't cause diamonds, because of proof irrelevance. And it seems that we won't get exponential blowup either. (Well, we do... but the base would not be as high as with the naive index on everything approach.)

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:07):

So is_comm_ring would still extend is_ring and is_comm_monoid as an old_structure.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:09):

I don't think is_comm_ring could extend is_comm_monoid if we explode the classes like this

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:10):

Why not?

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:10):

it means that a search for is_comm_monoid A <one> <add> would have to also search for is_comm_ring A <one> <add> ?

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:11):

Well, it would have to also search for has_mul A and has_zero A first. And if it found those, it could search for is_comm_ring A <zero> <one> <add> <mul>

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:12):

But if it doesn't find has_zero A, then it can forget about search for is_comm_ring

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:12):

That's similar to what we do now already with some mixins, right?

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:13):

I think it would still have to try to search for is_comm_ring A <zero'> <one> <add> <mul'> for every solution for zero' : has_zero A

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:13):

Sure, but search for all zero' : has_zero A will be very fast.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:13):

which means if there are multiple paths (even if they are defeq) this will result in combinatorial explosion

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:14):

Because in my hypothetical TC graph, there are no paths from some_type_class A to has_zero A

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:14):

So the search for has_zero A should be instant

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:14):

It will have 0 or 1 solutions

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:15):

And the same for every has_X A constant/unary/binary op.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:15):

what if the definition of has_zero for one type needs more things on another type? Or worse, a lawful class

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:16):

for example the has_one of polynomials needs has_zero and has_one on the base ring

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:18):

Sure, but won't that still be fast? I don't see how it is so different from what we are already doing. It will do structural recursion on the shape of A. If it sees polynomial R, then it searches for has_zero R and has_one R. That should hopefully bottom out pretty fast.

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:19):

I understand that it now has to do 2 searches, whereas in the current mathlib it has to do only 1 search.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:19):

well it seems untenable to get the "0 or 1" property in general

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:20):

Ok, I see your point, if the has_zero A would depend on some lawful class, then you would get multiple paths again

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:22):

This is an annoying issue.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:23):

I should say that I am in favor of the [[foo]] implicit quantification syntax, but I don't think we should overhaul the hierarchy to use it pervasively

view this post on Zulip Mario Carneiro (Nov 13 2020 at 19:24):

it hides problems, it doesn't solve them

view this post on Zulip Johan Commelin (Nov 13 2020 at 19:25):

This footnote of the blogpost seems to say that my idea isn't as bad as the nesting indices:

Note that the number of indices does not matter, like the fact that Monoid has both an Op and a Unit index. That just affects the constant factor. It’s the nesting of indices that gets us here.


Last updated: May 11 2021 at 15:12 UTC