mathlib

mathlib copied to clipboard

Quite often, the same group acts on the same space in many different ways. E.g., any group acts on itself in at least 3 different ways: g • h = g * h, g • h = h * g⁻¹, g • h = g * h * g⁻¹

I'm ready to work on this, but I'd prefer to know if you like this idea before starting.

Currently only group_action and sylow rely on mul_action; (semi)modules redefine has_scalar, and don't use mul_action. So, it should be relatively easy to refactor this.

With this in mind, I think that it's better to have a structure, not a class. I propose to use G ↷ α (\r) as notation. Then we can write

variables (G α : Type*) [group G] (a : G ↷ α)
def comp_hom {G' : Type*} [group G'] (f : G' → G) [is_group_hom f] : G' ↷ α := sorry