OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralizeContractor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Centralizing a contractor in an abelian-by-finite group

Conjugation on an abelian normal subgroup factors through the finite quotient. The product over that finite action is central and its action still has a finitely generated ascending base. This constructs the central element rather than assuming its existence.

  1. def OAI.PolycyclicRecognition.abelianNormalQuotientAction line 18
  2. theorem OAI.PolycyclicRecognition.abelianNormalQuotientAction_mk line 28
  3. theorem OAI.PolycyclicRecognition.exists_central_ascending_contractor line 33
  4. theorem OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase.pow line 52
  5. theorem OAI.PolycyclicRecognition.exists_central_ascending_contractor_of_finiteIndex line 67