complete_linear_ordered_add_comm_monoid

Stream: Is there code for X?

[Yaël Dillies]

Is there such a thing as a typeclass for complete linear orders which are also monoids? like linear_ordered_add_comm_monoid but with Sup and Inf.

[Yakov Pechersky]

I wish we had it. We don't. Closest thing I've seen is (conditionally_)complete_linear_order together with add_comm_monoid. There needs to be some refactoring of the architecture that marries the order hierarchy with the algebra hierarchy.

[Kevin Buzzard]

Is this not what @Damiano Testa embarked upon recently?

[Yakov Pechersky]

Do you mean that add_comm_monoid together with some contra|covariant_class (+) (<=) gets us most of the way there?

[Kevin Buzzard]

I guess I don't know what Yael wants the relationship between <= and + to be here. Presumably he wants more than [complete_linear_order X] [add_comm_monoid X].

[Yakov Pechersky]

You're right. ordered_add_comm_monoid is just add_comm_monoid, partial_order, and the covariant (+) (<=) and contravariant (+) (<).

[Yakov Pechersky]

So linear_ordered_add_comm_monoid should be constructable from the relevant pieces. Does that imply if one has complete_linear_order add_comm_monoid and the right contra/covariant_class, then the laws about Sup and Inf will work?

[Yaël Dillies]

Most likely, yes. But it would surely be better to have it as a class rather than calling the bare covariant_class.

[Yakov Pechersky]

Having it as its own class results is an X^N explosion, of partial/linear/conditionally_/complete_ x add_comm_monoid/semiring/ring/field x optionally with_top and/or with_bot. We can have all 16 or more. But there must be a better way. (This is also ignoring the comm_ part of the hierarchy.)