OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompletedIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete identity detects finite integral cohomological dimension

The class of the augmentation is transported into ordinary cohomology. Its successive connecting images are the syzygy identity classes. Vanishing of its image in complete cohomology therefore forces a projective syzygy. No vanishing from FP-infinity is assumed or asserted.

  1. def OAI.PolycyclicRecognition.normalizedGroupIdentityClass line 19
  2. theorem OAI.PolycyclicRecognition.normalizedGroupIdentityClass_comparison line 26
  3. theorem OAI.PolycyclicRecognition.normalizedSyzygyConnecting_identity line 35
  4. theorem OAI.PolycyclicRecognition.normalizedCohomologyForward_identity line 55
  5. def OAI.PolycyclicRecognition.completedIdentity line 71
  6. theorem OAI.PolycyclicRecognition.completedIdentity_eq_zero_iff line 75
  7. theorem OAI.PolycyclicRecognition.completedCohomology_trivial_subsingleton_iff line 92