Zulip Chat Archive

Stream: Is there code for X?

Topic: add_left_cancel_monoid


view this post on Zulip Sebastien Gouezel (Apr 10 2020 at 07:33):

I can't find the name of the structure in which addition is left-cancellative, like add_left_cancel_semigroup, but with a zero that plays well with the addition, like in an add_monoid. My natural guess would be add_left_cancel_monoid, but this doesn't exist. I just want to cover and groups, in fact, so any typeclass containing the two and with the two above properties would be enough for me.

By the way, this kind of question would not make sense with a structure like the one for topological spaces, with a rather small spine with the main players, and mixins to add all kinds of properties. I wish the algebraic hierarchy would also be like this...

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:35):

Why not just define it? It's not difficult and you get all the theorems for free

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:36):

class add_left_cancel_monoid A extends add_left_cancel_semigroup A, add_monoid A

add instances for groups and nat and you are ready to go

view this post on Zulip Sebastien Gouezel (Apr 10 2020 at 07:37):

Sure, but then I will also need to add an instance for nnreal, and maybe some other guy I am not thinking of.

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:37):

only if you need it

view this post on Zulip Sebastien Gouezel (Apr 10 2020 at 07:37):

With mixins, there would be no need to define a new class.

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:38):

I'm not convinced that this is actually saving much in this instance

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:38):

what I described seems pretty easy

view this post on Zulip Sebastien Gouezel (Apr 10 2020 at 07:38):

And the natural place for it is in core...

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:39):

No, you can do that anywhere

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:39):

there is no requirement that this be in core

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:39):

mathlib does this in a few places, inserting new classes in the middle of the hierarchy

view this post on Zulip Sebastien Gouezel (Apr 10 2020 at 07:40):

Sure, I am just saying that the natural place is in core, in init/algebra/groups.lean, close to add_monoid and add_left_cancel_semigroup.

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:40):

maybe, but that isn't a reason to complain about it, that's an organizational decision

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:41):

Actually it seems that the winds are blowing to take more of the algebraic hierarchy out of core anyway

view this post on Zulip Mario Carneiro (Apr 10 2020 at 07:43):

I don't want to be dismissive about mixins, but it is a complicated issue that affects many things and I think that any reinvestigation should be carefully thought out; single examples aren't enough unless the difference is really stark


Last updated: May 19 2021 at 02:10 UTC