Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_action_hom

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?

Reid Barton (Oct 28 2020 at 15:41):

Yes, docs#mul_action_hom

Reid Barton (Oct 28 2020 at 15:41):

aka X ->[M] Y

Adam Topaz (Oct 28 2020 at 15:41):

Thanks :)

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.

Eric Wieser (Oct 28 2020 at 15:43):

Should we change linear_map to extend mul_action_hom?

Adam Topaz (Oct 28 2020 at 15:46):

I'm too scared to touch linear_map...

Eric Wieser (Oct 28 2020 at 15:59):

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

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: Dec 20 2023 at 11:08 UTC