groups acting on sets

Stream: maths

[Kevin Buzzard]

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?

[Johan Commelin]

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

[Johan Commelin]

\bullet

[Kevin Buzzard]

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?

[Kenny Lau]

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

[Kenny Lau]

also when I did it myself I used \ci