OAI/GroupTheory/PolycyclicRecognition/Finiteness/LocallyFiniteRationalHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing a countable locally finite normal subgroup in rational homology

Finite-support representatives lie in finite subgroups, where transfer from the trivial subgroup kills positive rational homology. The normal-extension comparison then identifies ambient and quotient rational homology.

  1. theorem OAI.PolycyclicRecognition.locallyFinite_rational_homology_isZero line 20
  2. def OAI.PolycyclicRecognition.locallyFiniteKernelRationalHomologyIso line 34
  3. def OAI.PolycyclicRecognition.torsionNilpotentKernelRationalHomologyIso line 41