OAI/GroupTheory/PolycyclicRecognition/Finiteness/IntegerExtensionDuality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The cohomological dimension shift for an infinite cyclic extension

  1. def OAI.PolycyclicRecognition.integerExtensionResolution line 25
  2. def OAI.PolycyclicRecognition.integerExtensionMap line 32
  3. theorem OAI.PolycyclicRecognition.integerExtensionMap_homology line 39
  4. theorem OAI.PolycyclicRecognition.integerExtensionMap_homology_mono line 50
  5. def OAI.PolycyclicRecognition.integerExtensionCohomologyIso line 57
  6. theorem OAI.PolycyclicRecognition.integerExtensionCohomology_zero line 73
  7. theorem OAI.PolycyclicRecognition.poincareDuality_of_integerQuotient line 83