OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalExtensionTotalHomology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The normal-extension total complex computes ambient group homology

This comparison is proved from finite antidiagonal elimination, the exact bar resolution, and actual iterated coinvariants. No convergence or extension existence is introduced as a hypothesis.

  1. def OAI.PolycyclicRecognition.normalExtensionRowOpcyclesIso line 20
  2. def OAI.PolycyclicRecognition.normalExtensionTotalHomologyIso line 27