Ordered semirings

Stream: general

[Yaël Dillies]

Isn't a docs#canonically_ordered_semiring an docs#ordered_semiring?

import algebra.order.ring

instance (α : Type*) [canonically_ordered_comm_semiring α] : ordered_semiring α := by apply_instance

[Eric Wieser]

I assume you mean docs#canonically_ordered_comm_semiring

[Alex J. Best]

There was the thread https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology/near/225129909 but I don't know what the conclusion was or if its still relevant, perhaps @Damiano Testa can say more

[Yaël Dillies]

Oh, that's related to this old beast...

[Yaël Dillies]

I just want an ordered semiring where all elements are nonnegative.

[Eric Rodriguez]

take nat ;b for now, why can't you just say forall x, 0 < x?

[Yaël Dillies]

It's an instance.

[Eric Rodriguez]

Write it as a lemma and leave a todo?

[Yaël Dillies]

Eh, maybe. It's in #11329 and #11414.

[Eric Wieser]

I don't see the relevance to 11329?

[Eric Wieser]

Or even to #11414

[Yaël Dillies]

Have you seen the has_scalar instance I proposed?

[Notification Bot]

This topic was moved by Eric Wieser to #PR reviews > #11414 seminorm has_scalar instance

[Damiano Testa]

In case you are still wondering, I do not think that a canonically_ordered_comm_semiring is automatically an ordered_comm_semiring.

For instance, {0, 1} is a canonically ordered commutative semiring, where addition has 1 as an absorbing element: 1 + 1 = 1 (all remaining operations are forced by the notation and 0 < 1). However, this same equation, or rather 1 + 1 = 1 + 0, shows that this ring does not satifsy

add_le_add_left : ∀ (a b : R), a ≤ b → ∀ (c : R), c + a ≤ c + b

which is one of the fields of an ordered commutative semiring.

[Kevin Buzzard]

Semirings are just silly objects. I'd never heard of them until I started all this lean thing. I don't care that the natural numbers are a semiring, they're a subset of a ring. Nat gets too much love here. Long live int.

[Patrick Massot]

Kevin, we already had this conversation many times. Don't you sometimes use ideals in a commutative ring?

[Patrick Massot]

Maybe you sometimes multiply ideals or even add them. I've heard arithmetic people do that sometimes.

[Patrick Massot]

How do you call this algebraic structure on ideal R?

[Yaël Dillies]

I agree, Damiano, the current canonically_ordered_comm_semiring is not a ordered_comm_semiring. But should it be?

[Patrick Massot]

And now what about having ideal R acting on submodule R M? Don't you ever write M/IM?

[Patrick Massot]

How lucky we are to have a name for the algebraic structure that allows you to add submodules. It feels so good to talk about this semi-module over the semi-ring ideal R!

[David Wärn]

If we want to take semirings seriously, shouldn't we get rid of cancellation axioms like a * b = 0 → a = 0 ∨ b = 0 (from docs#canonically_ordered_comm_semiring) and a < b → 0 < c → c * a < c * b, a + b ≤ a + c → b ≤ c (from docs#ordered_semiring)? I think ideal R (for [comm_semiring R]) satisifes everything except these axioms, and it seems reasonable to call it a (canonically) ordered semiring

[Yaël Dillies]

In what stronger structure would you land those properties? We can't just let a < b → 0 < c → c * a < c * b go.

[David Wärn]

Right, I'm suggesting that it be moved to some other class, but I don't know the hierarchy well enough to say where. The example I have in mind is monoids and groups, with cancel monoids in between. Monoids are of course a lot more general than cancel monoids, and are often the right level of generality to work with. Semirings are supposed to be to rings what monoids are to groups, but the cancellation axioms make ordered_semiring more like cancel_monoid than monoid

[Yaël Dillies]

So you're suggesting ordered_cancel_semiring? That could do!

[Yakov Pechersky]

Can you provide it as a Prop mixin as some generalization of covariant_class?

[Yaël Dillies]

I expect so

[Yaël Dillies]

#YakovWillMixInAllYourTypeclasses

[Yakov Pechersky]

It might not be the right thing to do, but it's more composable/works with the pieces we already have

[Yakov Pechersky]

Rather than trying to insert another data-holding class somewhere in the hierarchy.

[Yakov Pechersky]

I'm only suggesting it here because we have the intersection of the order hierarchy and the algebraic hierarchy. In contrast, I've never suggested making commutativity of multiplication, or even worse, addition, a prop mixin.

[Yaël Dillies]

In this case, we already have
ordered_add_comm_monoid, ordered_add_cancel_comm_monoid
..., ordered_semiring
So the simplest thing now would be to complete the square
ordered_add_comm_monoid, ordered_add_cancel_comm_monoid
ordered_semiring, ordered_cancel_semiring

[Yaël Dillies]

But I'm not against switching to mixins.

[Damiano Testa]

Reorganizing the ordered hierarchy was what started me with the order refactor, but, honestly, I got overwhelmed part of the way through. I plan to pick it up again slowly, though.

[Damiano Testa]

My impression is that ordered semiring should refer to a semiring where addition and multiplication-by-positive elements should be monotone.

The somewhat circular implications between linear order, cancellative and strict monotonicity play some role, but secondary to the class design, in my opinion.

[Yaël Dillies]

Damiano Testa said:

I plan to pick it up again slowly, though.

That's great to hear! I feared you were not to be counted on anymore.

[Damiano Testa]

Thank you for the support! The refactor was a little overwhelming but I am glad that someone noticed that it had stopped!

[Yaël Dillies]

Bhavik can attest how sad I was you stopped!

[Damiano Testa]

Ok, sorry to have let you down! I will start PRing order stuff soon, then!

[Patrick Massot]

I wasn't worried about the order refactor but I noticed you weren't there anymore and it certainly make me sad.

[Bhavik Mehta]

Damiano Testa said:

Ok, sorry to have let you down! I will start PRing order stuff soon, then!

No pressure! But your work was certainly noticed and appreciated :)

[Damiano Testa]

Thank you all for your kind words: this community is really wonderful!

[Damiano Testa]

On a partially related note, is the partial order given by set-inclusion available on set_semiring? (See example below.)

This would lead to defining a canonically_ordered_comm_semiring on the set_semiring for any comm_monoid.

Since additions are absorbing, these are further examples of non ordered_comm_semirings that are canonically ordered. However, my reason for thinking about this is to simplify some argument with polynomials.

import algebra.pointwise
open set
open_locale pointwise

variables {X : Type*}

instance : has_le (set_semiring X) :=
{ le := λ x y, let x1 : set X := x in let y1 : set X := y in x1 ⊆ y1 }

instance : partial_order (set_semiring X) :=
{ le := (≤),
  le_refl := subset.refl,
  le_trans := λ a b c, subset.trans,
  le_antisymm := λ a b, subset.antisymm }

[Floris van Doorn]

You can do attribute [derive partial_order] set_semiring. This should probably be added to mathlib.

[Damiano Testa]

Great, I'll look into this and make a PR soon, then!

[Damiano Testa]

I finally got around to this, after receiving help on fixing permission issues!

#11567

Since this is the first time that I really use derive, I would be very happy if someone could confirm that this is what I was supposed to do!

Thanks!