feat(group_theory/group_action/subgroup): Conjugation action on subgroups of a group

[ChrisHughes24]

---

• depends on: [Merged by Bors] - feat(group_theory/subgroup): lemmas relating normalizer and map and comap #8458
• depends on: [Merged by Bors] - feat(group_theory/group_action/conj_act): conjugation action of groups #8627

[jcommelin]

Why the '? Is there another subgroup.mul_action? If so, should this one be a global instance?

[eric-wieser]

The other one is presumably (S : subgroup G) [mul_action G M] : mul_action S M which is just a naming conflict, not a semantic one.

[ChrisHughes24]

It doesn't really make much sense to define this action in terms of the conjugation action of groups on themselves since I had to make a type alias to define that action, but there's no need for a type alias here because there are no other actions that you might want to define.

[github-actions]

This PR/issue depends on:

• [Merged by Bors] - feat(group_theory/subgroup): lemmas relating normalizer and map and comap #8458
• [Merged by Bors] - feat(group_theory/group_action/conj_act): conjugation action of groups #8627
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

From what I gather, this action now exists as mul_action (mul_aut G) (subgroup G) instead of mul_action G (subgroup G) as offers this PR. @eric-wieser, is there a case for introducing this new action, or should we migrate the few exclusive lemmas from this PR to the mul_aut action?

[eric-wieser]

From what I gather, this action now exists as mul_action (mul_aut G) (subgroup G) instead of mul_action G (subgroup G) as offers this PR.

Correct

@eric-wieser, is there a case for introducing this new action, or should we migrate the few exclusive lemmas from this PR to the mul_aut action?

I don't like the idea of the mul_action G (subgroup G). mul_action (conj_act G) (subgroup G) ought to be safe though; it's entirely possible that instance can already be found by lean.

[ChrisHughes24]

From what I gather, this action now exists as mul_action (mul_aut G) (subgroup G) instead of mul_action G (subgroup G) as offers this PR. @eric-wieser, is there a case for introducing this new action, or should we migrate the few exclusive lemmas from this PR to the mul_aut action?

I think there is a need for this action, because mul_aut G is a different group with a different cardinality, so you won't be able to apply the orbit-stablizer theorem in the same way for example.

[YaelDillies]

The action in this PR isn't mul_action (mul_aut G) (subgroup G) but mul_action (conj_act G) (subgroup G), and conj_act G is the same group as G. The only downside so far is that the statement of stabilizer_eq_normalizer became more complicated, because you need to insert a map to_conj_act in there.

Somewhat relatingly, do we want a typeclass for an action to be a conjugation action? Of course G acts on subgroup G by conjugation, but so does any subgroup of G, and that isn't currently covered by this PR.

[ChrisHughes24]

I think it is covered by some instance saying if G acts on X so does any subgroup of G

[YaelDillies]

Yes, but some lemmas in this PR are about g • H where g : conj_act G and H : subgroup G, and they should still hold true if instead g : conj_act G' where G' : subgroup G.

[YaelDillies]

Sorry, why was this marked too-late? It compiled by the cutoff date. If it's because it's marked awaiting-author, let me mark it awaiting-review, since there are interesting lemmas to be saved.

[YaelDillies]

The lemmas added to other files are hopefully uncontroversial. For the ones in this file, I would like someone else's opinion. Maybe @eric-wieser?