OAI/GroupTheory/PolycyclicRecognition/Algebra/SmallCoefficientIdentityCycle.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unit identity cocycles in the coefficient-ring tower

The ordinary integral resolution remains the source of the cochains. Their coefficients are the same syzygies tensored with the small coefficient ring.

  1. abbrev OAI.PolycyclicRecognition.smallCoefficientTower line 19
  2. def OAI.PolycyclicRecognition.smallCoefficientIdentityCochain line 22
  3. theorem OAI.PolycyclicRecognition.smallCoefficientIdentityCochain_closed line 27
  4. def OAI.PolycyclicRecognition.smallCoefficientIdentityCycle line 33
  5. def OAI.PolycyclicRecognition.smallCoefficientIdentityClass line 40
  6. theorem OAI.PolycyclicRecognition.smallCoefficientIdentityCycle_projection line 46
  7. theorem OAI.PolycyclicRecognition.smallCoefficientIdentityClass_connecting line 54