OAI/GroupTheory/PolycyclicRecognition/Finiteness/ChosenIntegralResolution.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A resolution with finitely generated covers whenever available

The initial free term is the regular module. Every subsequent term covers the kernel of the preceding differential. The chosen presentation retains finite generation whenever that kernel is finitely generated.

  1. abbrev OAI.PolycyclicRecognition.integralFreeAugmentation line 19
  2. def OAI.PolycyclicRecognition.chosenIntegralKernelCover line 22
  3. def OAI.PolycyclicRecognition.chosenIntegralStep line 25
  4. theorem OAI.PolycyclicRecognition.chosenIntegralStep_comp line 29
  5. theorem OAI.PolycyclicRecognition.chosenIntegralStep_exact line 33
  6. def OAI.PolycyclicRecognition.chosenIntegralSuccessor line 49
  7. def OAI.PolycyclicRecognition.chosenIntegralResolutionComplex line 53
  8. def OAI.PolycyclicRecognition.chosenIntegralResolutionSuccessorIso line 58
  9. theorem OAI.PolycyclicRecognition.chosenIntegralResolution_step_finite line 63
  10. theorem OAI.PolycyclicRecognition.chosenIntegralResolution_projective line 69
  11. theorem OAI.PolycyclicRecognition.chosenIntegralResolution_d_succ line 78
  12. theorem OAI.PolycyclicRecognition.chosenIntegralResolution_exact line 84
  13. def OAI.PolycyclicRecognition.chosenIntegralResolutionAugmentation line 100
  14. theorem OAI.PolycyclicRecognition.chosenIntegralResolutionAugmentation_quasiIso line 108
  15. def OAI.PolycyclicRecognition.chosenIntegralResolution line 126