OAI/GroupTheory/PolycyclicRecognition/Finiteness/NilpotentCyclicDuality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The duality finiteness endgame for a nilpotent-by-cyclic group

No finiteness of the nilpotent kernel is assumed. The strict subgroup dimension bound identifies the ambient top degree, and its finite nonzero orientation homology forces stabilization of the nilpotent exhaustion.

  1. theorem OAI.PolycyclicRecognition.nilpotent_kernel_finitelyGenerated_of_integerQuotient line 24
  2. theorem OAI.PolycyclicRecognition.polycyclic_of_nilpotent_integerQuotient line 55