OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalAcyclicKernelHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quotient homology after removing a rationally acyclic normal subgroup

The comparison is assembled from the actual two bar directions and the degree-zero augmentation. No spectral-sequence collapse is assumed.

  1. def OAI.PolycyclicRecognition.normalExtensionColumnZeroOpcyclesIso line 20
  2. theorem OAI.PolycyclicRecognition.normalExtensionColumn_rational_isZero line 29
  3. def OAI.PolycyclicRecognition.rationalAcyclicKernelHomologyIso line 43