left/right cancelative semiring

Stream: Is there code for X?

[Damiano Testa]

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]

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]

docs#cancel_monoid_with_zero

[Johan Commelin]

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

[Johan Commelin]

I guess we want some sort of semidomain

[Kenny Lau]

why not?

[Johan Commelin]

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

[Johan Commelin]

Or are you suggesting an ingredient for a new class?

[Kenny Lau]

I guess

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

what's wrong with just making lots of combo classes

[Johan Commelin]

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

[Johan Commelin]

Potentially more like M * N * O * P

[Kenny Lau]

what's an M*N-problem?

[Johan Commelin]

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

[Johan Commelin]

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

But in practice M and N are small, right?

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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]

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

[Johan Commelin]

Note that linear_ordered_semiring exists, and it probably implies semidomain

[Damiano Testa]

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]

So why did we make PID and DVR into props?

[Mario Carneiro]

because people want to make mixins

[Johan Commelin]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Damiano Testa]

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]

My rule is: one type arg = one class

[Mario Carneiro]

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]

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

[Mario Carneiro]

yes

[Damiano Testa]

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]

Nope, it was what we later started calling semidomain

[Damiano Testa]

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]

and refactor lemmas for domain?

[Johan Commelin]

@Damiano Testa I think you an extend cancel_monoid_with_zero

[Mario Carneiro]

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

[Johan Commelin]

That gives you those cancel lemmas for free.

[Damiano Testa]

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

then?

[Kenny Lau]

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]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

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]

@Damiano Testa Yes, you can do that

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

Probably .. polynomial.nontrivial also exists

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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?

[Damiano Testa]

Ah, ok, you already answered! Thanks!