OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalizedIdentityClass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Identity cocycles in the normalized resolution

The projection onto the n-th syzygy is a cocycle. If its class vanishes in a positive degree, the next kernel inclusion splits; this gives a projective syzygy and hence finite integral dimension for the trivial coefficient.

  1. def OAI.PolycyclicRecognition.normalizedIdentityCycle line 18
  2. def OAI.PolycyclicRecognition.normalizedIdentityClass line 28
  3. theorem OAI.PolycyclicRecognition.normalizedIdentityCycle_projection line 34
  4. theorem OAI.PolycyclicRecognition.cochain_boundary_of_class_zero line 43
  5. theorem OAI.PolycyclicRecognition.normalizedIdentityClass_zero_projective_syzygy line 56
  6. theorem OAI.PolycyclicRecognition.finiteDimension_of_normalizedIdentityClass_zero line 77