OAI/GroupTheory/PolycyclicRecognition/Finiteness/DimensionFromRegularCohomology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The regular module detects finite cohomological dimension

For a finite resolution, vanishing with regular coefficients implies the same vanishing with free coefficients. Free covers and dimension shifting then give vanishing with every coefficient module.

  1. def OAI.PolycyclicRecognition.regularFreeCover line 23
  2. instance OAI.PolycyclicRecognition.regularFreeCover_epi line 26
  3. theorem OAI.PolycyclicRecognition.cohomology_vanishes_above_regular_bound line 36
  4. theorem OAI.PolycyclicRecognition.projectiveDimension_of_regular_cohomology_bound line 64
  5. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.cohomologicalDimension line 88
  6. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.dimension_unique line 94
  7. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.subgroup_dimension_le line 103