OrderedAddMonoid

Stream: maths

[Martin Dvořák]

We have OrderedAddCommMonoid which is certainly meaningful.

import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Order.BoundedOrder

class OrderedAddCommMonoid (α : Type*) extends AddCommMonoid α, PartialOrder α where
  /-- Addition is monotone in an `OrderedAddCommMonoid`. -/
  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b

Would the following class make any (mathematical) sense?

import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Order.BoundedOrder

class OrderedAddMonoid (α : Type*) extends AddMonoid α, PartialOrder α where
  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b
  protected add_le_add_right : ∀ a b : α, a ≤ b → ∀ c : α, a + c ≤ b + c

[Martin Dvořák]

Or OrderedMonoid rather.

[Yaël Dillies]

What's your use case?

[Yaël Dillies]

They are certainly people who study non-commutative orders, but those are pretty niche and we won't support them until they show up here.

[Martin Dvořák]

I don't have a use case, but I was thinking about lexicographical orderings on lists of ordered things.

[Martin Dvořák]

Actually no:

[1] < [1, 2]
[1, 3] > [1, 2, 3]

[Yaël Dillies]

Non-commutative orders do exist but they are pretty niche.

[Jireh Loreaux]

And the best ones involve star :laughing:

[Frédéric Dupuis]

Even then, addition is still commutative!

[Antoine Chambert-Loir]

Yaël Dillies said:

Non-commutative orders do exist but they are pretty niche.

In case of groups, they're not niche at all. For instance, the orderability of the braid group is an important theorem.

[Yuyang Zhao]

docs#Ordinal is an example.