## Stream: Is there code for X?

### Topic: left/right cancelative semiring

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

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

#### Kenny Lau (Oct 27 2020 at 07:25):

docs#cancel_monoid_with_zero

#### Johan Commelin (Oct 27 2020 at 07:29):

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

#### Johan Commelin (Oct 27 2020 at 07:29):

I guess we want some sort of semidomain

why not?

#### Johan Commelin (Oct 27 2020 at 07:30):

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

#### Johan Commelin (Oct 27 2020 at 07:30):

Or are you suggesting an ingredient for a new class?

I guess

#### Johan Commelin (Oct 27 2020 at 07:32):

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

#### Mario Carneiro (Oct 27 2020 at 07:35):

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

#### Mario Carneiro (Oct 27 2020 at 07:35):

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

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

#### Mario Carneiro (Oct 27 2020 at 07:36):

what's wrong with just making lots of combo classes

#### Johan Commelin (Oct 27 2020 at 07:37):

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

#### Johan Commelin (Oct 27 2020 at 07:37):

Potentially more like M * N * O * P

#### Kenny Lau (Oct 27 2020 at 07:37):

what's an M*N-problem?

#### Johan Commelin (Oct 27 2020 at 07:38):

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

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


#### Kevin Buzzard (Oct 27 2020 at 07:40):

But in practice M and N are small, right?

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

#### Johan Commelin (Oct 27 2020 at 07:42):

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

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

#### Mario Carneiro (Oct 27 2020 at 07:47):

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

#### Johan Commelin (Oct 27 2020 at 07:47):

Note that linear_ordered_semiring exists, and it probably implies semidomain

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

#### Johan Commelin (Oct 27 2020 at 07:47):

So why did we make PID and DVR into props?

#### Mario Carneiro (Oct 27 2020 at 07:48):

because people want to make mixins

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

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

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

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

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

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

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

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

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

#### Mario Carneiro (Oct 27 2020 at 07:53):

My rule is: one type arg = one class

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

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

yes

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

#### Johan Commelin (Oct 27 2020 at 07:56):

Nope, it was what we later started calling semidomain

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

#### Kenny Lau (Oct 27 2020 at 07:58):

and refactor lemmas for domain?

#### Johan Commelin (Oct 27 2020 at 07:58):

@Damiano Testa I think you an extend cancel_monoid_with_zero

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

#### Damiano Testa (Oct 27 2020 at 07:59):

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


then?

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


.

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

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

#### Damiano Testa (Oct 27 2020 at 09:10):

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

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

#### Johan Commelin (Oct 27 2020 at 09:48):

@Damiano Testa Yes, you can do that

#### Mario Carneiro (Oct 27 2020 at 09:48):

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

#### Johan Commelin (Oct 27 2020 at 09:48):

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


#### Johan Commelin (Oct 27 2020 at 09:49):

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

#### Damiano Testa (Oct 27 2020 at 09:49):

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

#### Johan Commelin (Oct 27 2020 at 09:49):

Probably .. polynomial.nontrivial also exists

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

#### Johan Commelin (Oct 27 2020 at 09:50):

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

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