OAI/GroupTheory/PolycyclicRecognition/Finiteness/LocalVirtualPolycyclicVanishing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Vanishing for locally virtually polycyclic height kernels

The finite-index passage uses the constructed relative trace, allowing torsion and avoiding a uniform bound on the ranks of finitely generated subgroups.

  1. theorem OAI.PolycyclicRecognition.IsVirtuallyPolycyclic.exists_poincareDuality_finiteIndex line 19
  2. theorem OAI.PolycyclicRecognition.smallCoefficient_virtuallyPolycyclic_finite_dimension line 32
  3. theorem OAI.PolycyclicRecognition.TypeFPInfinity.locallyVirtuallyPolycyclic_smallCoefficient_induction_vanishing line 42
  4. theorem OAI.PolycyclicRecognition.TypeFPInfinity.locallyVirtuallyNilpotent_smallCoefficient_induction_vanishing line 51