OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteIntegralHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integral homology finiteness from FP finiteness

Finite group-ring generators become finite integral generators after tensoring with a finite integral coefficient module and taking coinvariants. Since the integers are Noetherian, cycles and homology inherit finite generation.

  1. theorem OAI.PolycyclicRecognition.finite_coinvariantsTensor line 22
  2. theorem OAI.PolycyclicRecognition.finite_homology_of_finite_term line 44
  3. theorem OAI.PolycyclicRecognition.TypeFP.homology_finite line 53