OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentContractorEndgame.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The endgame from a contracting element in a nilpotent normal subgroup

The contracting condition is stated on the actual abelianization and is lifted by the proved nilpotent ascending-base theorem. Centrality modulo the nilpotent subgroup makes the generated cyclic extension normal.

  1. theorem OAI.PolycyclicRecognition.IsVirtuallyPolycyclic.of_surjective line 19
  2. theorem OAI.PolycyclicRecognition.cyclicJoin_eq_comap_zpowers line 27
  3. theorem OAI.PolycyclicRecognition.cyclicJoin_normal_of_central_quotient line 31
  4. def OAI.PolycyclicRecognition.ascendingData_cyclicJoin line 39
  5. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_nilpotent_contractor line 60
  6. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_nilpotent_abelian_contractor line 82