OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalExtensionBicomplex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The normal-extension bar bicomplex

One direction is the ambient resolution after normal coinvariants; the other is the quotient group's actual bar resolution. Its row homology is identified with actual quotient-group homology, and row degree zero with ordinary ambient coinvariants. No spectral-sequence convergence is assumed here.

  1. def OAI.PolycyclicRecognition.normalQuotientResolutionComplex line 21
  2. def OAI.PolycyclicRecognition.normalExtensionBicomplex line 26
  3. instance OAI.PolycyclicRecognition.normalQuotientResolutionComplex_projective line 32
  4. def OAI.PolycyclicRecognition.normalExtensionRowHomologyIso line 37
  5. def OAI.PolycyclicRecognition.normalExtensionRowZeroIso line 45