OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalCoefficientHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

FP finiteness with rationally finite coefficient modules

The integral coefficient module need not be finitely generated. Finiteness of its rationalization suffices: finite free covers give finite rational chain terms, and exact rationalization computes their rational homology.

  1. theorem OAI.PolycyclicRecognition.rational_coinvariantsTensor_finite line 23
  2. theorem OAI.PolycyclicRecognition.rational_homology_finite_of_term line 48
  3. theorem OAI.PolycyclicRecognition.TypeFP.rational_homology_finite line 56