Generalizing Group Action

Stream: mathlib4

[Qi Ge]

Hi all, I'm looking at Mathlib.GroupTheory.GroupAction.Hom and I would like to generalize MulActionHom DistribMulActionHom and MulSemiringActionHom to allow for compatibility with morphisms of monoids, just like the definition of LinearMap allows for a semilinear map w.r.t. a morphism of the coefficient ring. Is this something mathlib would like to incorporate or I should make separate Hom classes for my own project?

[Qi Ge]

Also, MulActionHom as it is currently defined isn't really for "homomorphisms of MulAction but instead it should be SMulHom, as MulActionHom currently does not assume the action is a monoid action but a generic type. It is true that there is no need to put in the extra parameter.

[Eric Wieser]

There is already at least one other person in the middle of such a project

[Qi Ge]

Great! Do you have any pointer for that?

[Jireh Loreaux]

@Eric Wieser you're not talking about me, are you?

[Eric Wieser]

I think it was maybe @Antoine Chambert-Loir? I really don't remember

[Antoine Chambert-Loir]

Yes, it is me. Everything is in the branch #SMulSemiHom . There is a PR in progress, #6057

[Antoine Chambert-Loir]

If you're willing to go on with that, feel free, because I don't really have the time now.

[Eric Wieser]

branch#SMulSemiHom

[Antoine Chambert-Loir]

@Qi Ge I managed to work a little bit on it yesterday night, and implemented all (I hope so) remarks by @Anne Baanen . Everytime something compiles, it goes further into building mathlib. This morning, I needed to fix something earlier (precisely as suggested by Anne) to make docs#CharacterSpace compile smoothly, and it now goes to reverting stupid modifications I had done in docs#StarHom… This is slow and a bit painful.

One thing that will need to be updated is how composition behaves, because for now, I do provide something analogous to docs#RingHomCompTriple but did not rewrite the latter in terms of the former. The reason is that the latter seems to play with TypeClasses to make a lot of equalities defeq, it is probably unreasonable to expect that in the overall generality.

Another thing that could be checked is having a consistent naming of similar functions map_smul, map_smul underscore sl, etc., possibly with primes, according to the function belonging to the structure or the class. I am not sure mathlib is consistent though, and I can't make my mind on what is reasonable. Maybe @Eric Wieser has an idea about this.