Zulip Chat Archive
Stream: new members
Topic: Conjugation action on subgroups
Christian Merten (Sep 25 2023 at 19:09):
In Mathlib/GroupTheory/GroupAction/ConjAct, the action of a group on itself by conjugation is defined. Is there also somewhere the conjugation action of a group on its subgroups, i.e. something like MulAction (ConjAct G) (Subgroup G)?
Yaël Dillies (Sep 25 2023 at 19:11):
It's automatically derived from docs#Subgroup.pointwiseMulAction
Yaël Dillies (Sep 25 2023 at 19:12):
Let me also mention that !3#8592 contains some results that might be of interest to you.
Christian Merten (Oct 28 2023 at 13:15):
Yaël Dillies said:
Let me also mention that !3#8592 contains some results that might be of interest to you.
Is this going to be merged and migrated to mathlib4 at some point? I would like to use some of the results in https://github.com/leanprover-community/mathlib4/pull/7991. Currently I just added the necessary lemmas.
Yaël Dillies (Oct 28 2023 at 13:23):
Well I'm in no position to tell you whether it will be merged to mathlib. But maybe @Eric Wieser is willing to review it?
Eric Wieser (Oct 28 2023 at 13:35):
I am not willing to do any further mathlib3 reviews until someone succeeds in running the script that updates #port-wiki
Christian Merten (Oct 28 2023 at 13:40):
Might it be a solution to just directly open a PR to mathlib4 with @Chris Hughes ported work, instead of merging into mathlib3 and then porting?
Eric Wieser (Oct 28 2023 at 13:49):
I think the porting route is probably easier, as long as someone runs that script
Kevin Buzzard (Oct 28 2023 at 13:56):
Has it now got to the point where the best way to make progress in practice is simply that someone manually ports that PR to mathlib4?
Eric Wieser (Oct 28 2023 at 14:10):
Someone needs to set up a GitHub token and run a python script
Eric Wieser (Oct 28 2023 at 14:10):
That is probably about the same amount of work as manually porting 2-3 PRs
Ruben Van de Velde (Oct 28 2023 at 14:11):
What python script?
Eric Wieser (Oct 28 2023 at 14:20):
The one linked to from the diagram in the readme of https://github.com/leanprover-community/mathlib-port-status
Eric Wieser (Oct 28 2023 at 14:21):
https://github.com/leanprover-community/mathlib4/blob/master/scripts/run_port_status.sh is the script
Christian Merten (Oct 28 2023 at 15:13):
Eric Wieser said:
https://github.com/leanprover-community/mathlib4/blob/master/scripts/run_port_status.sh is the script
With some minor modifications to the script it went through. What do I do with the output?
Eric Wieser (Oct 28 2023 at 15:14):
The script should have pushed the output automatically
Eric Wieser (Oct 28 2023 at 15:15):
Can you make PR with the modifications you made?
Christian Merten (Oct 28 2023 at 15:21):
Ah, I ran the python script directly for testing. Just running the shell script again and will then push the result and the modified script.
Christian Merten (Oct 28 2023 at 15:26):
Ah well I don't have permissions to push to mathlib.wiki
Christian Merten (Oct 28 2023 at 15:29):
Eric Wieser said:
Can you make PR with the modifications you made?
https://github.com/leanprover-community/mathlib4/pull/8001 for the modified script.
Eric Wieser (Oct 28 2023 at 15:31):
Christian Merten said:
Ah well I don't have permissions to push to mathlib.wiki
I've left some comments on your PR, and granted you access; can you make sure to address the comments first?
Christian Merten (Oct 28 2023 at 15:58):
I updated the wiki.
Eric Wieser (Oct 28 2023 at 16:08):
Thanks! #outofsync should update in 20 minutes
Last updated: Dec 20 2023 at 11:08 UTC