Complete Ordered AddCommMonoid

Stream: mathlib4

[Antoine Chambert-Loir]

I want to introduce an Ordered AddCommMonoid which is also a CompleteLinearOrder.
If I introduce successively [CompleteLinearOrder R] and [OrderedAddCommMonoid R], the two orderings on R
seem to be distinct…
How to do that?

[Anatole Dedecker]

I think the best solution is to use the fact that OrderedAddCommMonoid is really a bundled version of CovariantClass M M (· + ·) (· ≤ ·), and hope that whatever result you need from Mathlib actually assumes that instead of OrderedAddCommMonoid (which I think should always be the case?)

[Martin Dvořák]

I will probably end up doing the same (defining a typeclass for OrderedAddCommMonoid and CompleteLinearOrder together).

[Eric Wieser]

What types do you intend to cover with such a typeclass?

[Martin Dvořák]

Reals without multiplication.

[Eric Wieser]

Why not just use the reals?

[Martin Dvořák]

[messages in wrong order]

[Eric Wieser]

You can pretend the multiplication isn't there

[Martin Dvořák]

Actually, I want OrderedAddCommMonoid and CompleteLattice together.
Then I can consider tuples of real numbers with elementwise addition.

[Eric Wieser]

That sounds like a good motivation!

[Eric Wieser]

Though (tuples of) real numbers aren't a complete lattice

[Martin Dvořák]

I made a mistake. Tuples of EReal with elementwise addition would be the thing.

[Eric Wieser]

Note that to justify a new typeclass you should have at least two examples, but I assume they are:

• EReal
• Tuples of EReal (via Pi and Prod)

[Eric Wieser]

I think the answer to your question might be [CompleteLattice R] [AddCommMonoid R] [CovariantClass R R (· + ·) (· ≤ ·)] or similar

[Martin Dvořák]

Eric Wieser said:

Note that to justify a new typeclass you should have at least two examples, but I assume they are:

• EReal
• Tuples of EReal (via Pi and Prod)

Are you suggesting that CompleteOrderedAddCommMonoid should go to mathlib?

[Damiano Testa]

Maybe also ENNReals are an instance.

[Eric Wieser]

Are you suggesting that CompleteOrderedAddCommMonoid should go to mathlib?

I was, but now I'm suggesting that you can make do with [CompleteLattice R] [AddCommMonoid R] [CovariantClass R R (· + ·) (· ≤ ·)] for now

[Eric Wieser]

Because otherwise you're likely to find you want:

• CompleteOrderedAddCommMonoid
• CompleteOrderedAddCommGroup
• ConditionallyCompleteOrderedAddCommGroup
• ...

And the number of combinations quickly explodes

[Martin Dvořák]

Eric Wieser said:

I was, but now I'm suggesting that you can make do with [CompleteLattice R] [AddCommMonoid R] [CovariantClass R R (· + ·) (· ≤ ·)] for now

Is it guaranteed that
[CompleteLattice R] and [CovariantClass R R (· + ·) (· ≤ ·)]
talk about the same ≤
and that
[AddCommMonoid R] and [CovariantClass R R (· + ·) (· ≤ ·)]
talk about the same addition?

[Eric Wieser]

[CompleteLattice R] provides a ≤, CovariantClass talks about a ≤

[Eric Wieser]

The problem arises when two typeclasses provide a notation

[Eric Wieser]

You can tell that CovariantClass doesn't provide a ≤ because you needed the ≤ already to even state it

[Damiano Testa]

In fact, you can use any relation there and CovariantClass will work with that.

[Peter Nelson]

Is ENat not also an example?

[Peter Nelson]

I think there was a zulip thread about this not too long ago, but I’m on mobile