Zulip Chat Archive

Stream: maths

Topic: ordered commutative monoid


view this post on Zulip Patrick Massot (Apr 05 2019 at 17:30):

https://github.com/leanprover-community/mathlib/blob/3525d212e3b3166b2f3cf1a5dc89114962630168/src/algebra/ordered_group.lean#L17-L20:

/-- An ordered (additive) commutative monoid is a commutative monoid
  with a partial order such that addition is an order embedding, i.e.
  `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=

Why?!? Why isn't it called ordered_add_comm_monoid, and where are the actual ordered_comm_monoid?

view this post on Zulip Kevin Buzzard (Apr 06 2019 at 14:10):

And another thing @Mario Carneiro -- are you sure the a + b ≤ a + c ↔ b ≤ c claim follows from the axioms you give to this structure? I'm thinking about with_bot int with addition defined by -infty + x = -infty.

view this post on Zulip Patrick Massot (Apr 06 2019 at 14:11):

Yeah, this comment is actually false

view this post on Zulip Chris Hughes (Apr 06 2019 at 14:40):

That comment should be about ordered_cancel_comm_monoid, where a + b ≤ a + c → b ≤ cimplies cancellation

view this post on Zulip Patrick Massot (Apr 06 2019 at 14:56):

This area of mathlib is really a mess anyway. If you feel like cleaning it up then you can take whatever you want from https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/linear_ordered_comm_group.lean In particular I did a to_multiplicative by hand (search and replace) in order to get back my lemmas for actual commutative monoid (ie. with multiplicative notation) but of course the correct way is to patch mathlib to use multiplication and decorate everything with to_additive


Last updated: May 09 2021 at 09:11 UTC