OAI/GroupTheory/PolycyclicRecognition/Geometry/CommutatorBarBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact bar-boundary correction for a commutator

The antisymmetric two-letter chain is a cycle only for commuting letters. The correction below measures its failure in the actual group bar complex.

  1. def OAI.PolycyclicRecognition.commutatorBarChain line 18
  2. theorem OAI.PolycyclicRecognition.commutatorBarChain_boundary line 21
  3. def OAI.PolycyclicRecognition.commutatorBarPrimitive line 31
  4. theorem OAI.PolycyclicRecognition.commutatorBarPrimitive_boundary line 34
  5. theorem OAI.PolycyclicRecognition.commutatorBarChain_cycle_iff line 47