Commit 2022-08-17 14:53 c30985dc

View on Github →

feat(group_theory/transfer): The transfer homomorphism G →* center G (#14520) This PR constructs the transfer homomorphism G →* center G. The bulk of this PR is a messy computation giving a criterion (transfer_eq_pow) for when the transfer homomorphism is the power map. The same criterion can be used to prove Burnside's transfer theorem.

Estimated changes

Modified src/group_theory/group_action/quotient.lean

added theorem quotient_group.out'_conj_pow_minimal_period_mem

Modified src/group_theory/transfer.lean

added theorem monoid_hom.transfer_center_eq_pow

added theorem monoid_hom.transfer_center_pow'_apply

added theorem monoid_hom.transfer_center_pow_apply

modified theorem monoid_hom.transfer_def

added theorem monoid_hom.transfer_eq_pow

added theorem monoid_hom.transfer_eq_pow_aux

added theorem monoid_hom.transfer_eq_prod_quotient_orbit_rel_zpowers_quot