OAI/GroupTheory/PolycyclicRecognition/Finiteness/InfiniteCyclicDuality.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Integral Poincaré duality for an infinite cyclic group

  1. theorem OAI.PolycyclicRecognition.leftRegularHomEquiv_precomp_difference line 19
  2. def OAI.PolycyclicRecognition.cyclicHomDifference line 27
  3. def OAI.PolycyclicRecognition.cyclicHomAugmentation line 32
  4. theorem OAI.PolycyclicRecognition.cyclicHomAugmentation_surjective line 37
  5. theorem OAI.PolycyclicRecognition.cyclicHomAugmentation_exact line 46
  6. def OAI.PolycyclicRecognition.infiniteCyclicCochains line 63
  7. theorem OAI.PolycyclicRecognition.infiniteCyclicCochains_d_zero_one line 66
  8. theorem OAI.PolycyclicRecognition.infiniteCyclicCochains_d_one_two line 74
  9. theorem OAI.PolycyclicRecognition.infiniteCyclicCochains_isZero line 87
  10. theorem OAI.PolycyclicRecognition.infiniteCyclic_cohomology_zero line 93
  11. theorem OAI.PolycyclicRecognition.infiniteCyclic_cohomology_above_one line 104
  12. def OAI.PolycyclicRecognition.infiniteCyclic_cohomology_one_iso line 114
  13. theorem OAI.PolycyclicRecognition.poincareDuality_one_of_infinite_cyclic line 132