Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_action_hom


view this post on Zulip Adam Topaz (Oct 28 2020 at 15:40):

We have mul_action M X, which tells us when the monoid M has a multiplicative action on X. Do we have (bundled) morphisms of types endowed with a multiplicative action of M?

view this post on Zulip Reid Barton (Oct 28 2020 at 15:41):

Yes, docs#mul_action_hom

view this post on Zulip Reid Barton (Oct 28 2020 at 15:41):

aka X ->[M] Y

view this post on Zulip Adam Topaz (Oct 28 2020 at 15:41):

Thanks :)

view this post on Zulip Adam Topaz (Oct 28 2020 at 15:42):

I looked in the source of the file where mul_action was defined and gave up my search too quickly.

view this post on Zulip Eric Wieser (Oct 28 2020 at 15:43):

Should we change linear_map to extend mul_action_hom?

view this post on Zulip Adam Topaz (Oct 28 2020 at 15:46):

I'm too scared to touch linear_map...

view this post on Zulip Eric Wieser (Oct 28 2020 at 15:59):

I got away without touching linear_equiv... Do we have docs#smul_equiv?

view this post on Zulip Eric Wieser (Nov 03 2020 at 15:46):

Eric Wieser said:

Should we change linear_map to extend mul_action_hom?

Done in #4888


Last updated: May 07 2021 at 21:10 UTC