OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalZeroCoefficientHomology.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rationally zero coefficients have rationally zero homology

The proof uses the actual tensor-coinvariant terms of the bar complex. It requires no finite-generation assumption on the group or the coefficients.

  1. theorem OAI.PolycyclicRecognition.rational_tensor_isZero line 19
  2. theorem OAI.PolycyclicRecognition.rational_coinvariants_isZero line 34
  3. theorem OAI.PolycyclicRecognition.rational_coinvariantsTensor_isZero line 40
  4. theorem OAI.PolycyclicRecognition.rational_homology_isZero_of_term line 46
  5. theorem OAI.PolycyclicRecognition.rational_groupHomology_isZero_of_coefficient line 56