OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalBicomplexHomology.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rational homology of the finite total complex

Exact rationalization commutes with both homology directions, as well as the actual total homology. Every finiteness hypothesis below is explicit.

  1. def OAI.PolycyclicRecognition.rationalRowHomologyComplexIso line 19
  2. def OAI.PolycyclicRecognition.rationalBicomplexSecondPageIso line 29
  3. def OAI.PolycyclicRecognition.rationalBicomplexTotalHomologyIso line 36
  4. theorem OAI.PolycyclicRecognition.rational_total_homology_finite_of_secondPage line 43
  5. theorem OAI.PolycyclicRecognition.rational_total_homology_isZero_of_secondPage line 57