Commit 2025-02-25 16:16 1477914f
View on Github →chore: separate the automorphism groups from their tautological action (#22141) There is import tension between monoids of endomorphisms/groups of automorphisms and monoid/group actions:
- end/aut want to import actions to talk about their tautological action on the ground type.
- actions want to import end/aut because an action is the same thing as an hom to the correct end/aut monoid/group Currently, the first bullet point is done in the same file as the definition of end/aut, and the second bullet point is done in files interspersed across the files doing the first bullet point depending on which end/aut monoid/group you're talking about. This is a mess, so this PR makes sure that each of the following are in separate files:
- the definitions of end/aut
- the definition of actions
- the tautological action by end/aut, an action is the same thing as an hom to end/aut
Import replacement guide
Replace imports to your file according to
Mathlib.Algebra.Group.Aut
→Mathlib.Algebra.Group.Action.End
Mathlib.Algebra.Ring.Aut
→Mathlib.Algebra.Ring.Action.End
Then run#min_imports
.