OAI/GroupTheory/PolycyclicRecognition/Finiteness/PolyZDuality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integral duality along a torsion-free cyclic series

The comparison group needed in recognition can be chosen poly-Z. The cohomology shift for an infinite cyclic extension proves duality for this subgroup directly, without assuming the general polycyclic duality theorem.

  1. theorem OAI.PolycyclicRecognition.poincareDuality_of_infiniteCyclicQuotient line 20
  2. theorem OAI.PolycyclicRecognition.exists_poincareDuality_of_torsionFreeCyclicQuotient line 38
  3. theorem OAI.PolycyclicRecognition.IsPolyZ.exists_poincareDuality line 57
  4. theorem OAI.PolycyclicRecognition.IsPolycyclic.exists_poincareDuality_finiteIndex line 81