OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentPolyZ.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Torsion-free finitely generated nilpotent groups have poly-Z series

The center is a finitely generated integral lattice. Its quotient remains torsion-free, so induction on nilpotency class and concatenation of the two actual cyclic series give the result and integral Poincare duality.

  1. theorem OAI.PolycyclicRecognition.integralLattice_polyZ line 21
  2. theorem OAI.PolycyclicRecognition.abelian_polyZ_of_finitelyGenerated_torsionFree line 33
  3. theorem OAI.PolycyclicRecognition.nilpotent_polyZ_of_finitelyGenerated_torsionFree line 38
  4. theorem OAI.PolycyclicRecognition.nilpotent_poincareDuality_of_finitelyGenerated_torsionFree line 56