OAI/GroupTheory/PolycyclicRecognition/Algebra/SequentialRepresentationDiagram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Vanishing sequential systems and normalized syzygies

This packages only the sequential diagrams needed by the complete-cohomology construction. Vanishing means that each element is killed at a later stage.

  1. structure OAI.PolycyclicRecognition.SequentialRepresentationDiagram line 18
  2. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.Vanishes line 28
  3. abbrev OAI.PolycyclicRecognition.SequentialRepresentationDiagram.moduleMap line 31
  4. instance OAI.PolycyclicRecognition.SequentialRepresentationDiagram.moduleMap_directed line 33
  5. abbrev OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ModuleLimit line 46
  6. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.vanishes_iff_limit_subsingleton line 48
  7. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.mapFunctor line 72
  8. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.vanishes_normalizedFree line 78
  9. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.vanishes_normalizedSyzygy line 104
  10. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.vanishes_iteratedNormalizedSyzygy line 123