OAI/GroupTheory/PolycyclicRecognition/Finiteness/CokernelResolution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite projective resolution for the cokernel in the cyclic extension

  1. abbrev OAI.PolycyclicRecognition.cokernelResolutionMap line 17
  2. def OAI.PolycyclicRecognition.cokernelResolutionAugmentation line 19
  3. theorem OAI.PolycyclicRecognition.cokernelResolutionAugmentation_apply line 26
  4. theorem OAI.PolycyclicRecognition.cokernelResolutionAugmentation_surjective line 34
  5. theorem OAI.PolycyclicRecognition.cokernelResolutionAugmentation_boundary line 43
  6. theorem OAI.PolycyclicRecognition.cokernelResolutionAugmentation_quasiIso line 66
  7. def OAI.PolycyclicRecognition.cokernelProjectiveResolution line 84