OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteDimensionTorsionFree.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite integral cohomological dimension excludes torsion

Restriction gives a dimension bound on every cyclic subgroup. Its periodic integral cohomology contradicts that bound if the subgroup is nontrivial finite.

  1. theorem OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension.torsionFree line 19
  2. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.torsionFree line 37