OAI/GroupTheory/PolycyclicRecognition/Geometry/IntegralAbelianBarBoundary.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Filling one-chains in an abelian group

A finite integral one-chain with zero sum in the group is an actual bar boundary. This is the degree-one comparison, with the primitive retained.

  1. def OAI.PolycyclicRecognition.abelianBarSum line 16
  2. theorem OAI.PolycyclicRecognition.integralH1AbelianizationEquiv_abelian_chain line 19
  3. theorem OAI.PolycyclicRecognition.abelianBar_boundary_of_sum_zero line 33