Zulip Chat Archive

Stream: Is there code for X?

Topic: left/right cancelative semiring


view this post on Zulip Damiano Testa (Oct 27 2020 at 07:15):

Dear All,

does mathlib have the notion of a nontrivial, left and right cancelative semiring? This would probably be a class extending semiring, nontrivial, mul_left_cancel, mul_right_cancel.

I am asking since, as far as I can tell, the polynomial semiring with coefficients in has this property, but is not a domain/integral_domain. I do not necessarily insist on not assuming commutativity of multiplication, though this property seems to play very little role in proofs. I would be more interested in not assuming existence of opposites (additive inverses) in the semiring, since there are cases where working with ℕ[x] = polynomial ℕ is important.

Note: the left/right cancelative property is stronger than the property of not having zero divisors, but is equivalent to it, under the existence of additive inverses.

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:24):

I don't think this exists, but note that you can mix certain classes. So a cancel_semiring R can be mixed with nontrivial R.

view this post on Zulip Kenny Lau (Oct 27 2020 at 07:25):

docs#cancel_monoid_with_zero

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:29):

@Kenny Lau but you can't mix that with a ring structure

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:29):

I guess we want some sort of semidomain

view this post on Zulip Kenny Lau (Oct 27 2020 at 07:29):

why not?

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:30):

You'll get two multiplications on your type, right?

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:30):

Or are you suggesting an ingredient for a new class?

view this post on Zulip Kenny Lau (Oct 27 2020 at 07:31):

I guess

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:32):

@Mario Carneiro Does it make sense to refactor domain to be a mixin Prop?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:35):

I don't know, it seems like a slippery slope

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:35):

it makes using domains more annoying and also makes typeclass search more expensive

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:36):

Dear @Johan Commelin @Kenny Lau , what you suggest is essentially what I had in mind!

I am happy with having a new class and the name semidomain seems appropriate!

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:36):

what's wrong with just making lots of combo classes

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:37):

It's a bit of an M * N-problem, right?

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:37):

Potentially more like M * N * O * P

view this post on Zulip Kenny Lau (Oct 27 2020 at 07:37):

what's an M*N-problem?

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:38):

Well, with combo classes you need M * N of them, but with mixins only M + N.

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:40):

@Damiano Testa My guess is that this will do what you want:

section

set_option old_structure_cmd true

class semidomain (R : Type*) extends cancel_monoid_with_zero R, semiring R.

end

view this post on Zulip Kevin Buzzard (Oct 27 2020 at 07:40):

But in practice M and N are small, right?

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:41):

Well, someone will come along, and ask for ordered_semidomain, and we also need comm_ versions of both

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:42):

@Damiano Testa You'll want to provide an instance from domain to semidomain

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:46):

I will try it out! For the moment, I do not have a real and urgent need for it, but I am thinking in terms of Hilbert's 17th problem, about sums of squares, where the coefficients change between and ℝ₊.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:47):

Not only M and N are small, we don't need the complete product

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:47):

Note that linear_ordered_semiring exists, and it probably implies semidomain

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:47):

since it seems that domain is used very little in mathlib (at least, without also assuming existence of opposites), it might make sense to set it up from the start so that all these results will be directly proven in the more context.

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:47):

So why did we make PID and DVR into props?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:48):

because people want to make mixins

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:48):

Damiano Testa said:

since it seems that domain is used very little in mathlib (at least, without also assuming existence of opposites), it might make sense to set it up from the start so that all these results will be directly proven in the more context.

Introducing a definition like semidomain brings with it the obligation to write a 250 line file with all the basic lemmas (-;

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:49):

Johan Commelin said:

Note that linear_ordered_semiring exists, and it probably implies semidomain

What I had in mind was indeed always an ordered base ring, but the order is not the property that I was thinking of using.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:49):

As far as I know we haven't actually hit any significant issues with combo classing everything, except that you have a lot of obscurely named classes

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:50):

Johan Commelin said:

Introducing a definition like semidomain brings with it the obligation to write a 250 line file with all the basic lemmas (-;

hmmm

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:50):

It's one line to define a new combo class, you don't even need any API to start using it

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:51):

Generally the only lemmas you will have for a combo class are those that were generalized from a more restrictive class, and the new ones you want to state

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:52):

Ok, I will go for the minimal choice of simply defining a new class extending all the properties that I want and will see what I can do with that. If it works well, I may produce a PR. I just wanted to make sure that this new class did not already exist, so that I did not have to make it up in my own.

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:53):

I think it is a very good idea that something like [algebra R A] is a mixin

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:53):

If all are happy, I will call it semidomain since I quite like the name and it seems fairly descriptive of what it is.

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:53):

My rule is: one type arg = one class

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:54):

for more type args you will potentially need one class per subset of the type args (so for two type args like module/algebra you have [foo R] [bar A] [baz R A])

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:55):

So you think we should have fin_dim_algebra K L to avoid [algebra K L] [finite_dimensional K L]?

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:56):

yes

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:56):

Johan Commelin said:

I don't think this exists, but note that you can mix certain classes. So a cancel_semiring R can be mixed with nontrivial R.

Does a cancel_semiring already exist? I could not find it...

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:56):

Nope, it was what we later started calling semidomain

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:57):

Ok, I will extend semiring, nontrivial and add two further properties that look exactly like mul_left_cancel and mul_right_cancel (and are called the same)!

view this post on Zulip Kenny Lau (Oct 27 2020 at 07:58):

and refactor lemmas for domain?

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:58):

@Damiano Testa I think you an extend cancel_monoid_with_zero

view this post on Zulip Mario Carneiro (Oct 27 2020 at 07:58):

It's best to call them the same thing if they are identical, so that you can mix them together in combo classes using ..s

view this post on Zulip Johan Commelin (Oct 27 2020 at 07:58):

That gives you those cancel lemmas for free.

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:59):

class semidomain (R : Type*) : cancel_monoid_with_zero R, nontrivial R

then?

view this post on Zulip Kenny Lau (Oct 27 2020 at 07:59):

Johan Commelin said:

Damiano Testa My guess is that this will do what you want:

section

set_option old_structure_cmd true

class semidomain (R : Type*) extends cancel_monoid_with_zero R, semiring R.

end

.

view this post on Zulip Damiano Testa (Oct 27 2020 at 07:59):

(I have a meeting right now: I will look back at this thread once the meeting is over!)

view this post on Zulip Johan Commelin (Oct 27 2020 at 08:00):

Maybe nontrivial should also be added... from a maths point of view the zero ring is probably not a semidomain

view this post on Zulip Damiano Testa (Oct 27 2020 at 09:10):

I definitely want nontrivial to be part of the definition! Thank you all for your help!

view this post on Zulip Damiano Testa (Oct 27 2020 at 09:47):

After I typed the definition

class semidomain (R : Type*) extends cancel_monoid_with_zero R, semiring R, nontrivial R

I would then like to show that if R is a semidomain, than also polynomial R is a semidomain:

lemma semidomain_pol (R : Type*) [semidomain R] : semidomain (polynomial R) :=

Is there a way of using the fact that polynomial R already is a semiring and so I only need to define cancel_monoid_with_zero and nontrivial? Also, many of the cancel_monoid_with_zero properties should already be available and if I could recycle them, it would be awesome!

Thanks!

view this post on Zulip Johan Commelin (Oct 27 2020 at 09:48):

@Damiano Testa Yes, you can do that

view this post on Zulip Mario Carneiro (Oct 27 2020 at 09:48):

yes, in the instance you can write {field := bla, ..polynomial.semiring}

view this post on Zulip Johan Commelin (Oct 27 2020 at 09:48):

instance [semidomain R] : semidomain (polynomial R) :=
{ some_field := _,
  .. polynomial.semiring }

view this post on Zulip Johan Commelin (Oct 27 2020 at 09:49):

Maybe you need polynomial.semiring R, depending on whether it takes an explicit argument or not.

view this post on Zulip Damiano Testa (Oct 27 2020 at 09:49):

Ah, I never used instance! I will play around with it! Thanks!

view this post on Zulip Johan Commelin (Oct 27 2020 at 09:49):

Probably .. polynomial.nontrivial also exists

view this post on Zulip Johan Commelin (Oct 27 2020 at 09:50):

instance is just like def and lemma, but with the extra feature that it adds the declaration to the typeclass system

view this post on Zulip Johan Commelin (Oct 27 2020 at 09:50):

So that later on semidomain (polynomial R) can be found automatically by Lean

view this post on Zulip Damiano Testa (Oct 27 2020 at 09:51):

Johan Commelin said:

instance is just like def and lemma, but with the extra feature that it adds the declaration to the typeclass system

This means that if I then type polynomial R and R is a semidomain, Lean will know that polynomial R is a semidomain as well?

view this post on Zulip Damiano Testa (Oct 27 2020 at 09:51):

Ah, ok, you already answered! Thanks!


Last updated: May 16 2021 at 05:21 UTC