OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicQuotientDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Infinite cyclic extensions of groups of finite integral dimension

Finite generation of the kernel's projective resolution is unnecessary for the dimension bound. Truncate an arbitrary resolution before induction.

  1. theorem OAI.PolycyclicRecognition.cohomologicalDimension_le_of_infiniteCyclicQuotient line 18
  2. theorem OAI.PolycyclicRecognition.finiteCohomologicalDimension_of_infiniteCyclicQuotient line 30