OAI/GroupTheory/PolycyclicRecognition/Finiteness/QuotientCoinvariantsFiniteness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite generation after normal-subgroup coinvariants

The quotient group acts on the actual coinvariants of each resolution term. When the quotient is finitely generated abelian, its noetherian group ring makes homology finite as well. No homological tameness implication is assumed.

  1. theorem OAI.PolycyclicRecognition.finite_rep_descent line 23
  2. theorem OAI.PolycyclicRecognition.finite_quotientCoinvariants line 51
  3. theorem OAI.PolycyclicRecognition.finite_rep_shortComplex_homology line 60
  4. theorem OAI.PolycyclicRecognition.finite_rep_chain_homology line 70
  5. instance OAI.PolycyclicRecognition.quotientCoinvariants_additive line 76
  6. theorem OAI.PolycyclicRecognition.typeFP_quotientCoinvariants_homology line 84