OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalizedProjectiveResolution.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The projective resolution determined by normalized free covers

Its quotient syzygy in degree n is the actual n-fold normalized kernel used in the complete-cohomology construction.

  1. def OAI.PolycyclicRecognition.normalizedFreeStep line 17
  2. theorem OAI.PolycyclicRecognition.normalizedFreeStep_comp line 21
  3. theorem OAI.PolycyclicRecognition.normalizedFreeStep_exact line 25
  4. def OAI.PolycyclicRecognition.normalizedResolutionTerm line 40
  5. def OAI.PolycyclicRecognition.normalizedResolutionDifferential line 43
  6. def OAI.PolycyclicRecognition.normalizedResolutionComplex line 47
  7. theorem OAI.PolycyclicRecognition.normalizedResolutionComplex_d line 57
  8. instance OAI.PolycyclicRecognition.normalizedResolutionComplex_projective line 62
  9. theorem OAI.PolycyclicRecognition.normalizedResolutionComplex_exact line 66
  10. def OAI.PolycyclicRecognition.normalizedResolutionAugmentation line 86
  11. theorem OAI.PolycyclicRecognition.normalizedResolutionAugmentation_quasiIso line 93
  12. def OAI.PolycyclicRecognition.normalizedProjectiveResolution line 107