OAI/GroupTheory/PolycyclicRecognition/Finiteness/HomologyExhaustion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Homology vanishing passes from an exhaustive sequence of subgroups

The proof uses finite support directly: a cycle lifts to a stage, injectivity of its bar inclusion detects that it is a cycle there, and a local filling maps to a global filling. No spectral sequence or colimit hypothesis is used.

  1. theorem OAI.PolycyclicRecognition.groupHomology_isZero_of_exhaustion line 20
  2. theorem OAI.PolycyclicRecognition.nilpotent_exists_uniform_homology_bound line 54