OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalEigencharacters.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite-index stabilizers of normal-subgroup eigenspaces

Conjugation permutes the common eigenvalue functions of a normal subgroup. There are only finitely many nonzero common eigenspaces. Consequently every one of them is invariant under a subgroup of finite index in the ambient group. This separates the finite permutation from the linear action.

  1. def OAI.PolycyclicRecognition.conjugateWeightPerm line 24
  2. def OAI.PolycyclicRecognition.normalCommonEigenspace line 53
  3. theorem OAI.PolycyclicRecognition.mem_normalCommonEigenspace line 57
  4. theorem OAI.PolycyclicRecognition.normalCommonEigenspace_conjugate line 61
  5. theorem OAI.PolycyclicRecognition.normalCommonEigenspace_conjugate_ne_bot line 77
  6. theorem OAI.PolycyclicRecognition.exists_finiteIndex_preserving_commonEigenspace line 86
  7. theorem OAI.PolycyclicRecognition.exists_finiteIndex_nonzero_commonEigenspace line 108