OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentTorsionQuotientEndgame.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional endgame modulo nilpotent torsion

Finite rational kernel rank gives a characteristic locally finite normal subgroup whose removal leaves finite virtual integral cohomological dimension. Neither the finiteness of this torsion subgroup nor the rank implication from ambient FP-infinity is asserted here.

  1. def OAI.PolycyclicRecognition.normalNilpotentTorsionSubgroup line 20
  2. instance OAI.PolycyclicRecognition.normalNilpotentTorsionSubgroup_normal line 23
  3. theorem OAI.PolycyclicRecognition.nilpotent_abelianization_mod_torsion_virtual_finite_dimension line 27