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.AutMathlib.Algebra.Group.Action.End
  • Mathlib.Algebra.Ring.AutMathlib.Algebra.Ring.Action.End Then run #min_imports.

Estimated changes

deleted theorem AddAut.apply_inv_self
deleted theorem AddAut.coe_mul
deleted theorem AddAut.coe_one
deleted def AddAut.congr
deleted def AddAut.conj
deleted theorem AddAut.conj_apply
deleted theorem AddAut.conj_inv_apply
deleted theorem AddAut.conj_symm_apply
deleted theorem AddAut.inv_apply_self
deleted theorem AddAut.inv_def
deleted theorem AddAut.mul_apply
deleted theorem AddAut.mul_def
deleted theorem AddAut.neg_conj_apply
deleted theorem AddAut.one_apply
deleted theorem AddAut.one_def
deleted def AddAut.toPerm
deleted def AddAutAdditive
deleted theorem MulAut.apply_inv_self
deleted theorem MulAut.coe_mul
deleted theorem MulAut.coe_one
deleted def MulAut.congr
deleted def MulAut.conj
deleted theorem MulAut.conj_apply
deleted theorem MulAut.conj_inv_apply
deleted theorem MulAut.conj_symm_apply
deleted theorem MulAut.inv_apply_self
deleted theorem MulAut.inv_def
deleted theorem MulAut.mul_apply
deleted theorem MulAut.mul_def
deleted theorem MulAut.one_apply
deleted theorem MulAut.one_def
deleted def MulAut.toPerm
deleted def MulAut
added theorem Equiv.Perm.addLeft_add
added theorem Equiv.Perm.coe_mul
added theorem Equiv.Perm.coe_one
added theorem Equiv.Perm.coe_pow
added theorem Equiv.Perm.default_eq
added theorem Equiv.Perm.inv_addLeft
added theorem Equiv.Perm.inv_def
added theorem Equiv.Perm.inv_mulLeft
added theorem Equiv.Perm.mulLeft_mul
added theorem Equiv.Perm.mulLeft_one
added theorem Equiv.Perm.mul_apply
added theorem Equiv.Perm.mul_def
added theorem Equiv.Perm.mul_refl
added theorem Equiv.Perm.mul_symm
added theorem Equiv.Perm.one_apply
added theorem Equiv.Perm.one_def
added theorem Equiv.Perm.one_symm
added theorem Equiv.Perm.one_trans
added theorem Equiv.Perm.pow_addLeft
added theorem Equiv.Perm.pow_mulLeft
added theorem Equiv.Perm.refl_inv
added theorem Equiv.Perm.refl_mul
added theorem Equiv.Perm.swap_inv
added theorem Equiv.Perm.symm_mul
added theorem Equiv.Perm.trans_one
deleted theorem Equiv.Perm.apply_inv_self
deleted theorem Equiv.Perm.coe_mul
deleted theorem Equiv.Perm.coe_one
deleted theorem Equiv.Perm.coe_pow
deleted theorem Equiv.Perm.default_eq
deleted theorem Equiv.Perm.eq_inv_iff_eq
deleted theorem Equiv.Perm.inv_apply_self
deleted theorem Equiv.Perm.inv_def
deleted theorem Equiv.Perm.inv_eq_iff_eq
deleted theorem Equiv.Perm.inv_trans_self
deleted theorem Equiv.Perm.iterate_eq_pow
deleted theorem Equiv.Perm.mul_apply
deleted theorem Equiv.Perm.mul_def
deleted theorem Equiv.Perm.mul_refl
deleted theorem Equiv.Perm.mul_symm
deleted theorem Equiv.Perm.one_apply
deleted theorem Equiv.Perm.one_def
deleted theorem Equiv.Perm.one_symm
deleted theorem Equiv.Perm.one_trans
deleted theorem Equiv.Perm.refl_inv
deleted theorem Equiv.Perm.refl_mul
deleted theorem Equiv.Perm.self_trans_inv
deleted theorem Equiv.Perm.sumCongr_inv
deleted theorem Equiv.Perm.sumCongr_mul
deleted theorem Equiv.Perm.sumCongr_one
deleted theorem Equiv.Perm.symm_mul
deleted theorem Equiv.Perm.trans_one
deleted theorem Equiv.addLeft_add
deleted theorem Equiv.addLeft_zero
deleted theorem Equiv.addRight_add
deleted theorem Equiv.addRight_zero
deleted theorem Equiv.inv_addLeft
deleted theorem Equiv.inv_addRight
deleted theorem Equiv.inv_mulLeft
deleted theorem Equiv.inv_mulRight
deleted theorem Equiv.mulLeft_mul
deleted theorem Equiv.mulLeft_one
deleted theorem Equiv.mulRight_mul
deleted theorem Equiv.mulRight_one
deleted theorem Equiv.mul_swap_eq_iff
deleted theorem Equiv.mul_swap_involutive
deleted theorem Equiv.mul_swap_mul_self
deleted theorem Equiv.pow_addLeft
deleted theorem Equiv.pow_addRight
deleted theorem Equiv.pow_mulLeft
deleted theorem Equiv.pow_mulRight
deleted theorem Equiv.swap_apply_apply
deleted theorem Equiv.swap_eq_one_iff
deleted theorem Equiv.swap_inv
deleted theorem Equiv.swap_mul_eq_iff
deleted theorem Equiv.swap_mul_involutive
deleted theorem Equiv.swap_mul_self
deleted theorem Equiv.swap_mul_self_mul
deleted theorem Equiv.zpow_addLeft
deleted theorem Equiv.zpow_addRight
deleted theorem Equiv.zpow_mulLeft
deleted theorem Equiv.zpow_mulRight
deleted def MonoidHom.toHomPerm