Typeclass for compatible group actions

Stream: mathlib4

[Thomas Browning]

Given [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G R] [MulSemiringAction G S], is there a typeclass that imposes compatibility between these actions? I.e., g • algebraMap R S r = algebraMap R S (g • r)?

This condition is equivalent to g • (r • 1) = (g • r) • 1, so IsScalarTower G R S almost works, except that imposing g • (r • s) = (g • r) • s is too strong since implies that G fixes S pointwise (set r = 1).

(This comes up in PR #27053 where I need to impose this compatibility condition but don't know of a nice typeclass for it).

[Thomas Browning]

I'm guessing no, since the lemma docs#algebraMap.coe_smul is stated in terms of IsScalarTower (in which case, should there be a new typeclass made for this?).

[Thomas Browning]

In terms of •, I think the desired condition is just a distributive version of IsScalarTower: g • (r • s) = (g • r) • (g • s).

[Aaron Liu]

Thomas Browning said:

This condition is equivalent to g • (r • 1) = (g • r) • 1, so IsScalarTower G R S almost works, except that imposing g • (r • s) = (g • r) • s is too strong since implies that G fixes S pointwise (set r = 1).

I set r = 1, now what? How do I get the fixing pointwise?

[Aaron Liu]

oh I get it now

[Andrew Yang]

I had this in one of my PRs for this exact reason here. But then I figured I didn't need it in that specific PR so I removed it.

[Andrew Yang]

If you are adding this typeclass then I am happy to review it. If not I'll open a new PR containing the deleted content in the above commit.

[Thomas Browning]

Nice! I won't have time to get around to this for a few days, so feel free to PR it if you have the time.

[Thomas Browning]

Here's a first stab at this: #30991