Zulip Chat Archive

Stream: general

Topic: Duplicate mul_action defs


view this post on Zulip Eric Wieser (Mar 28 2021 at 22:19):

I just realized that the docs#monoid_hom.comp_mul_action def I introduced duplicates docs#mul_action.comp_hom. Which name is better?

view this post on Zulip Eric Wieser (Mar 28 2021 at 22:21):

I don't think we have docs#semimodule.comp_hom, but I could rename docs#ring_hom.comp_semimodule

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:00):

I prefer mul_action.comp_hom because we take (\bu) ∘ f, not the other way.

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 03:01):

I'm going to remove your def in branch#smul-to-add for now. Please tell me if I should revert this.

view this post on Zulip Eric Wieser (Mar 29 2021 at 08:16):

The downside of comp_hom is that it doesn't work with dot notation

view this post on Zulip Eric Wieser (Mar 29 2021 at 08:18):

But I agree with the order argument

view this post on Zulip Eric Wieser (Mar 29 2021 at 10:26):

/poll Which name is better

  • mul_action.comp_hom, semimodule.comp_hom (matches the order of composition)
  • monoid_hom.comp_mul_action, ring_hom.comp_semimodule (works with dot notation)

view this post on Zulip Johan Commelin (Mar 29 2021 at 10:29):

I prefer the first one, but mostly just because I use it most, and hence I'm accustomed to it.

view this post on Zulip Anne Baanen (Mar 29 2021 at 10:33):

My intuition says the first one is better, but there is also the family of docs#function.injective.semigroup, which seems to give precendence to the second choice. So I'm officially undecided.

view this post on Zulip Eric Wieser (Mar 29 2021 at 10:38):

Since both of you agree with Yury, let's just rename them

view this post on Zulip Eric Wieser (Mar 29 2021 at 10:39):

Although it probably makes sense to split that change out of Yury's PR, and possibly to merge #6909 first

view this post on Zulip Eric Wieser (Mar 29 2021 at 15:00):

Done in #6942, which folds in #6909 since it's basically all the same anyway.


Last updated: May 11 2021 at 22:14 UTC