Conjugation Action

Stream: maths

[Aaron Anderson]

I'd like to implement conjugation as a mul_action (so that, among other things, we can use orbit-stabilizer theory to study centralizers) and there are a few ideas which come to mind as to how to do this:

[Aaron Anderson]

• Define a type synonym
• Have this be the default instance of mul_action (units M) M for any monoid M.

[Aaron Anderson]

The second seems ideal to me, but I fear that I'll run into trouble. It seems that there isn't a global instance already of the form mul_action (units M) M, but are there any special cases where that does pop up?

[Aaron Anderson]

Will the coercion of units M to M make this intractible?

[Adam Topaz]

So you want a • b to mean "conjugate b by a"? This feels really confusing to me, purely from a notation point of view.

[Aaron Anderson]

Only if a is a units M... otherwise we will have something like a • conj_action b

[Adam Topaz]

But still, I would tend to think that a • b should mean ↑a * b when a : units M and b : M.

[Aaron Anderson]

Perhaps it can be a local instance throughout a particular file?

[Adam Topaz]

I've seen some notation like ${}^a b$ for $a \cdot b \cdot a^{-1}$.

[Adam Topaz]

And similarly $b^a = a^{-1} \cdot b \cdot a$.

[Adam Topaz]

Can we try to emulate something like that?

[Adam Topaz]

$b^a$ is nice because it's a right action so you have the nice formula $(b^a)^c = b^{ac}$

[Aaron Anderson]

If someone knows how to make a mul_action have that notation, I can work with it. But if I want to, say, refer to a stabilizer in a given group action, I'm pretty sure I need at least a local mul_action instance, in which the action is denoted with •

[Adam Topaz]

Yeah, I understand, that's a fair point.

[Adam Topaz]

Maybe a general approach is to define a mul_action as a def whenever you have a morphism of monoids from a monoid $M$ to the endomorphism monoid of $N$, in the usual way. This would be a special case of that, and you can make it a local instance when needed.

[Adam Topaz]

Unfortunately....

import algebra

variables {M : Type*} [monoid M]

example : monoid (M →* M) := by apply_instance -- fails

[Eric Wieser]

I have an open PR that chooses a different default mul_action (units M) ...

[Aaron Anderson]

Eric Wieser said:

I have an open PR that chooses a different default mul_action (units M) ...

oooof

[Adam Topaz]

Is it the multiplication of the coercion?

[Eric Wieser]

Mainly because we already have lots of lemmas about it

[Eric Wieser]

Yes

[Aaron Anderson]

back to type-synonym land I crawl

[Eric Wieser]

#7438

[Eric Wieser]

Strictly it's the action of the coercion, not the multiplication

[Adam Topaz]

gotcha

[Eric Wieser]

Eg units rat has the "obvious" action on fin 3 -> rat

[Adam Topaz]

That's great.

[Adam Topaz]

Next you should define projective spaces!

[Eric Wieser]

Responding to an earlier message:

import algebra.group.hom

variables {M : Type*} [monoid M]

example : monoid (monoid.End M) := by apply_instance -- works?

[Eric Wieser]

docs#monoid.End.monoid

[Adam Topaz]

Hence

import algebra

variables {M : Type*} [monoid M]

example : monoid (M →* M) := show monoid (monoid.End M), by apply_instance -- works :)

[Adam Topaz]

(I know...)

[Eric Wieser]

(for anyone who doesn't know, that conflicts with docs#monoid_hom.comm_monoid)

[Adam Topaz]

Eric Wieser said:

(for anyone who doesn't, that conflicts with docs#monoid_hom.comm_monoid)

aka the "pointwise" structure