OAI/GroupTheory/PolycyclicRecognition/Finiteness/CoefficientResolutionHomology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Computing homology from a resolution of the coefficient representation

The two actual bar directions identify derived coinvariants of an arbitrary coefficient representation with its usual group homology. This is the coefficient comparison needed when a locally finite kernel is removed.

  1. def OAI.PolycyclicRecognition.coefficientBarBicomplex line 18
  2. def OAI.PolycyclicRecognition.coefficientBarRowOpcyclesIso line 22
  3. def OAI.PolycyclicRecognition.coefficientBarColumnHomologyIso line 28
  4. def OAI.PolycyclicRecognition.coefficientBarTotalRowHomologyIso line 45
  5. def OAI.PolycyclicRecognition.coefficientResolutionZeroHomologyIso line 60
  6. def OAI.PolycyclicRecognition.coefficientResolutionColumnOpcyclesIso line 64
  7. def OAI.PolycyclicRecognition.coefficientResolutionHomologyIso line 72