Ordered algebraic structures?

[andreasabel]

I was looking for partially ordered monoid (POMonoid) but could not find it. This is a chimera of a monoid and a partial order such that the composition operation of the monoid is monotone, i.e., we have x*y <= x'*y' whenever x<=x' and y<=y'.

Do we have ordered algebraic structures yet?
If not where should we place them in the module hierarchy?

[JacquesCarette]

No, they don't exist yet. I would be tempted to create an Algebra.Ordered hierarchy for them (yes, even though here the order is partial.)

[MatthewDaggitt]

Agreed. 'Algebra.Ordered' sounds good to me as well.

…

On Thu, 20 Jan 2022, 07:23 Jacques Carette, ***@***.***> wrote: No, they don't exist yet. I would be tempted to create an Algebra.Ordered hierarchy for them (yes, even though here the order is partial.) — Reply to this email directly, view it on GitHub <#1694 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAP26EVQ2DLAO5C3OHZ32NTUW75D3ANCNFSM5ML5GJPA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[laMudri]

I sense a combinatorial explosion, but as it happens I've also been using this specific combination (algebraic structures in the category of posets). Any plans for when people want more order features (e.g, meets, joins, decidability)?

[MatthewDaggitt]

@Taneb any reason why you closed this? I think best to keep it up until someone actually implements the said proposal!

[MatthewDaggitt]

I sense a combinatorial explosion, but as it happens I've also been using this specific combination (algebraic structures in the category of posets). Any plans for when people want more order features (e.g, meets, joins, decidability)?

Well people haven't requested the decidable ones for even basic algebraic structures yet. Unsure about meets and joins, but I imagine we'd have a .Decidable sub-hierarchy, e.g. Algebra.Decidable and Algebra.Ordered.Decidable...

[Taneb]

@Taneb any reason why you closed this? I think best to keep it up until someone actually implements the said proposal!

Oh, I didn't realise I had done that! I think I must have pressed the button accidentally on my phone. Many apologies.