Zulip Chat Archive

Stream: maths

Topic: groups acting on sets


view this post on Zulip Kevin Buzzard (Jan 31 2019 at 15:42):

Did we ever get groups acting on sets? [or even monoids acting on sets?]. The reason I ask is that I just tried to define groups acting on abelian groups and I realised I can't use * because the action is G -> M -> M. Has a decision been made about notation for groups acting on anything other than themselves?

view this post on Zulip Johan Commelin (Jan 31 2019 at 15:45):

Yes, these are in mathlib, and you want to use smul, I think.

view this post on Zulip Johan Commelin (Jan 31 2019 at 15:45):

\bullet

view this post on Zulip Kevin Buzzard (Jan 31 2019 at 15:55):

Apparently it's \bu now. And I have to import algebra.module to get the notation :-) It should be some far more primitive thing. Is the fact that the notation is defined in algebra.module evidence that we don't have groups acting on sets yet?

view this post on Zulip Kenny Lau (Jan 31 2019 at 16:20):

Did we ever get groups acting on sets? [or even monoids acting on sets?]. The reason I ask is that I just tried to define groups acting on abelian groups and I realised I can't use * because the action is G -> M -> M. Has a decision been made about notation for groups acting on anything other than themselves?

is_group_action

view this post on Zulip Kenny Lau (Jan 31 2019 at 16:20):

also when I did it myself I used \ci


Last updated: May 10 2021 at 08:14 UTC