leanprover-community
RFC: turn `mul_action` into a `structure`
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
The obvious downside is that we loose access to the notation. I would really like to write g • x for random actions. But I understand that in concrete situations this might cause pain.
@jcommelin We can use something like g •[a] x, and leave g • x to (semi-)modules scalar multiplication.
If some file deals with only one group action, you can always introduce a local notation.
Ok, fair enough. I was actually hoping to make (semi)modules extend actions. But maybe that's not such a good idea. @ChrisHughes24 @digama0 @kckennylau Do you have any opinions?
Are you handling multiple actions within the same lemma? If not, I'd rather keep it as it is right now.
@ChrisHughes24 I thought that classes are mostly for “canonical” structures. I mean, as soon as you want to deal with specific actions instead of abstract ones, in many cases you can't define them as instances in the library. Indeed, if you have instances for all 3 actions of a group on itself mentioned above, then the meaning of g • h depends on which instance comes first. So, you have to define specific actions using def, then use local attribute [instance] in a section that wants to deal with this action. For me, this ruins the main reason to use classes.
Another reason to use structure is that this way one can write a.orbit x, a.stabilizer x etc. instead of thinking each time what type(s) must be written explicitly.
P.S.: I remember that sometimes it is useful to work with left and right action of a group on itself at the same time, but I don't remember any good specific example.
Another way to handle multiple actions of the same group on the same set is to use type synonyms, for example
def G_with_left_action : Type := G
instance : group_action G G_with_left_action := ...
def G_with_conjugation_action : Type := G
instance : group_action G G_with_conjugation_action := ...
This is pretty natural because we think of G with the action of left multiplication and G with the action of conjugation as being different G-sets (even if mathematical notation tends not to distinguish them in this case).
Or for your example of comp_hom, we can define
def res {G G' : Type*} [group G] [group G'] (f : G' → G) [is_group_hom f]
(α : Type*) [group_action G α] := α
instance : group_action G' (res f α) := ...
The most common scenario is probably that one has a variable group acting on a variable module through a single variable action, and then one defines group cohomology or whatever. The type class style is well adapted to this type of situation. I'm not sure whether "just use local notation" is an adequate substitute.
There's also nothing that prevents a mix of styles--you can accept values of types that are classes with a () or {} parameter and pass them around explicitly, though it may be more difficult to design the library so that this is not awkward.
@rwbarton It seems that we have very different examples in mind. For me (as a dynamical systems person), it is very common to have, e.g., multiplicative int acting on some space in a few different ways (i.e., by iterates of different maps). In this case I don't want to have different types for different actions.
My proposal is to have g • x for “canonical” actions (e.g., modules over rings), and g •[a] x for non-canonical actions. If you have only one action, it should be easy to write
variables (a : G ↷ α)
local attribute [instance] a.to_has_scalar
example: g • x = x
rw [a.mul_smul]
If you have several actions in the same file,
abbreviation a₁ := left_mul_action G
abbreviation a₂ := conj_action G
example: g •[a₁] x = g •[a₂] x
I am now convinced that we need a better way of doing this. I guess another example of a non-canonical action to study is the flow of a differential equation. You shouldn't have to rename the reals for every ODE you study. The algebra type class formalizes the notion of a canonical ring homomorphism, whilst still keeping normal homomorphisms. I guess we could do the same for actions.
Currently only
group_actionandsylowrely onmul_action; (semi)modules redefinehas_scalar, and don't usemul_action. So, it should be relatively easy to refactor this.
It seems that (now) semimodule extends distrib_mul_action which extends mul_action. Probably it changed since June 2019.
My proposal is to have
g • xfor “canonical” actions (e.g., modules over rings), andg •[a] xfor non-canonical actions. If you have only one action, it should be easy to write
If we could have a class and a structure peacefully coexisting, that would seem best to me. I've been working on localizations of mul_actions (which I would prefer anyways to call "modules" somehow, with the lack of additive structure clear from context) and I think it would be a bit strange to refer to the monoid actions explicitly everywhere.
variables (a : G ↷ α) local attribute [instance] a.to_has_scalar
Does this actually work? I would have thought you can only attach attributes to declarations.
I wrote most comments here when I knew much less about mathlib. Now I think that we should have a structure and lemmas that take a structure argument in the mul_action namespace, then import (most of) the lemmas to the top namespace while replacing (a : mul_action G α) with [mul_action G α]. I hope that the latter step can be automated.