OAI/GroupTheory/PolycyclicRecognition/Finiteness/StableResolutionLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The limiting identity in a projective resolution

The limiting identity vanishes precisely when one syzygy is projective. This proves the finite-dimension detection step; it does not assert that FP-infinity or elementary amenability makes this identity vanish.

  1. abbrev OAI.PolycyclicRecognition.resolutionStableEnd line 20
  2. def OAI.PolycyclicRecognition.resolutionStableForward line 31
  3. instance OAI.PolycyclicRecognition.resolutionStableForward_directed line 46
  4. def OAI.PolycyclicRecognition.resolutionStableIdentity line 51
  5. theorem OAI.PolycyclicRecognition.resolutionStableForward_identity line 54
  6. abbrev OAI.PolycyclicRecognition.StableResolutionLimit line 68
  7. def OAI.PolycyclicRecognition.stableResolutionLimitingIdentity line 71
  8. theorem OAI.PolycyclicRecognition.stableResolutionLimitingIdentity_eq_zero_iff line 75