OAI/GroupTheory/PolycyclicRecognition/Finiteness/ExteriorSquareHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Second homology covers twice the exterior square

This holds for arbitrary abelian groups, including torsion. Inverting two turns the explicit map into a surjection; no finite-rank assumption is imposed here.

  1. abbrev OAI.PolycyclicRecognition.exteriorSquareHomology line 15
  2. theorem OAI.PolycyclicRecognition.exteriorSquareHomology_antisymmetric line 19
  3. theorem OAI.PolycyclicRecognition.exteriorSquareHomology_covers_twice line 25