feat(algebra/group/GroupModule): basic definitions of bundled modules over a group

[semorrison]

Since @kbuzzard was interested a prototype of group modules, I thought I'd write a version too. This is just a draft PR, and perhaps can wait until either it has more content, or someone actually wants it, but I think might be useful for discussion regarding bundled objects and using the category theory library with them.

The basic definition here is

structure GroupModule (G : Group.{u₁}) :=
(V : AddCommGroup.{u₁})
(ρ : G ⟶ Group.of (Aut V))

and it's all "follow your nose" from there.

[semorrison]

Actually, I couldn't resist generalising a bit, from AddCommGroup to an arbitrary 𝕍, so these definitions will work equally well for groups acting on Ab or on vector spaces.

[jcommelin]

@semorrison This is a "Draft" PR. What does that mean? Do you want to merge this, or do you first want more comments?

[semorrison]

Mostly I wanted to try out the "Draft" feature.

Somehow I really don't want to argue that this is the best definition for a GroupModule G. There are many many definitional choices that could be made here. This is a sketch of how you might set up the category after making one such choice.

Certainly we want to provide the equivalence between GroupModule (Module k) G and Module (monoid_algebra k G) at some point. This can't quite be done in this PR, as monoid_algebra is in #2135 which hasn't landed.

In any case, I'll click "Ready for review", and we can continue this discussion.

[jcommelin]

Ok, I'll tag this RFC for now, and focus on other PRs first. Please feel free to ping me if you want me to look at it again.

[semorrison]

I've completely rewritten this, and will reopen a separate PR later.