## Stream: maths

### Topic: getting a ring from an integral domain

#### 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))
(@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))
(@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)))


#### 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?

#### Adam Topaz (Nov 13 2020 at 14:53):

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

Oh yes!

#### Filippo A. E. Nuccio (Nov 13 2020 at 14:53):

Thank you so much! I now realize the problem.

No problem :)

#### Filippo A. E. Nuccio (Nov 13 2020 at 14:53):

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

#### Filippo A. E. Nuccio (Nov 13 2020 at 14:54):

So that I can add hR : is_integral_domain R?

I'm not sure.

#### 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...

#### Adam Topaz (Nov 13 2020 at 14:55):

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

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

#### Filippo A. E. Nuccio (Nov 13 2020 at 14:56):

But I can add it in the variables definition.

#### Filippo A. E. Nuccio (Nov 13 2020 at 15:10):

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?

I think so.

#### Adam Topaz (Nov 13 2020 at 15:17):

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

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


Very nice!

#### Johan Commelin (Nov 13 2020 at 15:31):

is_integral_domain exists.

Thanks!

#### 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.

#### Adam Topaz (Nov 13 2020 at 17:27):

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

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

#### 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.

#### 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!

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

#### Eric Wieser (Nov 13 2020 at 18:31):

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

#### 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.

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

#### Mario Carneiro (Nov 13 2020 at 18:39):

there is an issue for this

#### Mario Carneiro (Nov 13 2020 at 18:40):

leanprover/lean#1522

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

#### Adam Topaz (Nov 13 2020 at 18:41):

Yeah, I guess you're right @Johan Commelin

#### Adam Topaz (Nov 13 2020 at 18:41):

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

#### Mario Carneiro (Nov 13 2020 at 18:41):

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

Why?

#### 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.

#### Mario Carneiro (Nov 13 2020 at 18:43):

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

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

#### Eric Wieser (Nov 13 2020 at 18:43):

Right - all the to_has_add parts of typeclass search would vanish

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

#### Johan Commelin (Nov 13 2020 at 18:48):

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

#### 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.

#### 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.)

#### 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.

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

Why not?

#### 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> ?

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

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

#### Johan Commelin (Nov 13 2020 at 19:12):

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

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

#### Johan Commelin (Nov 13 2020 at 19:13):

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

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

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

#### Johan Commelin (Nov 13 2020 at 19:14):

So the search for has_zero A should be instant

#### Johan Commelin (Nov 13 2020 at 19:14):

It will have 0 or 1 solutions

#### Johan Commelin (Nov 13 2020 at 19:15):

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

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

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

#### 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.

#### 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.

#### Mario Carneiro (Nov 13 2020 at 19:19):

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

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

#### Johan Commelin (Nov 13 2020 at 19:22):

This is an annoying issue.

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

#### Mario Carneiro (Nov 13 2020 at 19:24):

it hides problems, it doesn't solve them

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