OAI/GroupTheory/PolycyclicRecognition/Algebra/ListBarShuffle.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The one- and two-letter shuffle operators on abelian bar chains

List coordinates make the insertion homotopies recursive. Degree restrictions will identify these operators with the ordinary finite-tuple bar complex.

  1. abbrev OAI.PolycyclicRecognition.ListBarChain line 16
  2. def OAI.PolycyclicRecognition.listBarPrepend line 18
  3. theorem OAI.PolycyclicRecognition.listBarPrepend_single line 21
  4. def OAI.PolycyclicRecognition.listBarBoundaryValue line 28
  5. def OAI.PolycyclicRecognition.listBarBoundary line 34
  6. theorem OAI.PolycyclicRecognition.listBarBoundary_single line 37
  7. def OAI.PolycyclicRecognition.listBarInsertValue line 43
  8. def OAI.PolycyclicRecognition.listBarInsert line 47
  9. theorem OAI.PolycyclicRecognition.listBarInsert_single line 50
  10. def OAI.PolycyclicRecognition.listBarPairValue line 54
  11. def OAI.PolycyclicRecognition.listBarPair line 59
  12. theorem OAI.PolycyclicRecognition.listBarPair_single line 62
  13. theorem OAI.PolycyclicRecognition.listBarInsert_prepend line 66
  14. theorem OAI.PolycyclicRecognition.listBarPair_prepend line 76