units.mul_action' diamond

Stream: general

[Reid Barton]

units.mul_action' is weird anyways, and at odds with the usual meaning of a group acting on a monoid (where the formula should be $(g.m)^{-1} = g.m^{-1}$; maybe just delete it?

[Reid Barton]

e.g., Galois groups acting on fields is a more typical example

[Eric Wieser]

The action is useful because it saves us having to duplicate all the lemmas about groups acting on monoids for coerced units acting on monoids

[Eric Wieser]

Besides, your complaint is equally valid against monoid.to_mul_action when G=M, right?

[Reid Barton]

These are not actions of groups on monoids in the first place

[Eric Wieser]

Are you using "monoid" to also mean "not a group"?

[Reid Barton]

I'm not sure what the right setup is here, but it's definitely weird/confusing to call this an "action"

[Reid Barton]

No, a monoid could be a group

[Reid Barton]

Or, it's a group acting on a set, and the set is a monoid, but it's not a group acting on a monoid

[Reid Barton]

But anyways the point is that if a group is acting on a monoid, then it also acts on the units (of course, just like it acts on anything built from the monoid) but not by the units.mul_action' formula

[Reid Barton]

Eric Wieser said:

Besides, your complaint is equally valid against monoid.to_mul_action when G=M, right?

Yes, this is also not an action, it should be something like "M acts on its underlying set"

[Eric Wieser]

I'm not sure I see the problem still. units.mul_action just says "if there's a group that acts on a set and the set is a monoid, then that group acts in the same way when the set is the units of a monoid"

[Eric Wieser]

I think what you're after is a units.mul_distrib_mul_action, which is probably missing, but wouldn't be incompatible.

[Eric Wieser]

The $(g.m)^{-1} = g.m^{-1}$ you ask for is docs#smul_inv', which is about mul_distrib_mul_action

[Reid Barton]

Eric Wieser said:

I think what you're after is a units.mul_distrib_mul_action

Yes, this is the good notion!

[Eric Wieser]

mul_distrib_mul_action is a pretty lousy name, but no one suggested a better name when I PR'd it

[Eric Wieser]

I just PR'd that instance in #10480

[Eric Wieser]

It has all the same problems as described with mul_action upthread, but we should be able to fix both instances at once in the future, since the new one carries no new data.

[Reid Barton]

But those are the wrong conditions!

[Reid Barton]

It should be simply [group G] [monoid M] [mul_distrib_mul_action G M]

[Reid Barton]

[smul_comm_class G M M] [is_scalar_tower G M M] will normally not be true

[Eric Wieser]

Right, those are a workaround for a problem with right-vs-left actions

[Reid Barton]

e.g. imagine the symmetric group on 3 letters acting on $k[X,Y,Z]$, or whatever

[Eric Wieser]

I think the correct assumptions are [group G] [monoid M] [mul_distrib_mul_action G M] [mul_distrib_mul_action Gᵒᵖ M] [is_symmetric_smul G M], where the last two are mathematically meaningless noise to make typeclass diamonds go away and make the generalization to mul_action work

[Reid Barton]

This only makes sense if $g$ acts on the right by $g^{-1}$

[Reid Barton]

Reid Barton said:

e.g. imagine the symmetric group on 3 letters acting on $k[X,Y,Z]$, or whatever

this is a boring example for units, so throw in $X^{-1}$, $Y^{-1}$, $Z^{-1}$ too

[Eric Wieser]

Perhaps. My plan was to try introducing the is_symmetric_smul typeclass once #10457 is in, and then revisit whether it helps with this units action later

[Reid Barton]

it's usually not going to happen that both $g.(x*y) = (g.x)*(g.y)$ and also $g.(x*y) = (g.x)*y$ for instance

[Reid Barton]

The first one is an action of a group on a monoid, that's why it's so confusing to talk about an action in the context of the second one

[Reid Barton]

The more normal way to express the hypotheses of mul_action' is that you have a homomorphism $\varphi : G \to M$ and you are writing $gm$ for $\varphi(g)m$

[Reid Barton]

and also the homomorphism is central

[Eric Wieser]

Reid Barton said:

it's usually not going to happen that both $g.(x*y) = (g.x)*(g.y)$ and also $g.(x*y) = (g.x)*y$ for instance

Yes, I agree - I think this is good evidence that something is wrong with the assumptions of mul_action (which we already knew), but I don't think #10480 is harmful, as it doesn't make anything more wrong, it just adds proofs that things are off.

[Reid Barton]

do you mean units.mul_action'?

[Reid Barton]

mul_action by itself is fine, it's just a group acting on a set

[Reid Barton]

If something is wrong then it would be more helpful to add documentation to that effect

[Reid Barton]

I am not sure whether we agree about what is wrong.