OAI/GroupTheory/PolycyclicRecognition/Algebra/VirtualNilpotentByAbelian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-index nilpotent-by-abelian structure in finite integral dimension

The maximal nilpotent normal subgroup has finite-dimensional rational central layers. After passing to finite index the derived action on those layers is uniformly unipotent. The centralizer criterion then puts that derived subgroup inside the nilpotent normal subgroup itself.

  1. theorem OAI.PolycyclicRecognition.exists_finiteIndex_commutator_le_maximal_nilpotent line 22
  2. theorem OAI.PolycyclicRecognition.exists_nilpotent_normal_finiteIndex_commutator line 62