OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalHomologyDimension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Detecting dimension using rational homology with coefficients

Shapiro's lemma passes a uniform bound to subgroups. The orientation module detects the dimension of an integral Poincare duality group even after rationalization. No finiteness of coefficient representations is required.

  1. def OAI.PolycyclicRecognition.RationalHomologyDimensionLE line 22
  2. theorem OAI.PolycyclicRecognition.RationalHomologyDimensionLE.subgroup line 26
  3. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.dimension_le_of_rational_homology_bound line 34