getting a ring from an integral domain

Stream: maths

[Filippo A. E. Nuccio]

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

[Adam Topaz]

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]

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

[Filippo A. E. Nuccio]

Oh yes!

[Filippo A. E. Nuccio]

Thank you so much! I now realize the problem.

[Adam Topaz]

No problem :)

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

So that I can add hR : is_integral_domain R?

[Adam Topaz]

I'm not sure.

[Filippo A. E. Nuccio]

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]

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

[Filippo A. E. Nuccio]

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]

But I can add it in the variables definition.

[Filippo A. E. Nuccio]

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?

[Adam Topaz]

I think so.

[Adam Topaz]

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

[Adam Topaz]

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

[Filippo A. E. Nuccio]

Very nice!

[Johan Commelin]

is_integral_domain exists.

[Filippo A. E. Nuccio]

Thanks!

[Kevin Buzzard]

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]

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

[Adam Topaz]

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]

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]

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

[Eric Wieser]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Mario Carneiro]

there is an issue for this

[Mario Carneiro]

leanprover/lean#1522

[Johan Commelin]

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

Yeah, I guess you're right @Johan Commelin

[Adam Topaz]

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

[Mario Carneiro]

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

[Johan Commelin]

Why?

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

Right - all the to_has_add parts of typeclass search would vanish

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Why not?

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

So the search for has_zero A should be instant

[Johan Commelin]

It will have 0 or 1 solutions

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

This is an annoying issue.

[Mario Carneiro]

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]

it hides problems, it doesn't solve them

[Johan Commelin]

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.