OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianSecondHomologyPairing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bilinear pairings descend to second homology of an abelian group

The antisymmetric bar cycle on two commuting elements evaluates to twice the pairing. This will supply the exterior-square quotient used in the character obstruction.

  1. abbrev OAI.PolycyclicRecognition.integralTrivialCoefficient line 19
  2. def OAI.PolycyclicRecognition.bilinearPairingChains line 21
  3. theorem OAI.PolycyclicRecognition.bilinearPairingChains_single line 25
  4. theorem OAI.PolycyclicRecognition.bilinearPairingChains_boundary line 31
  5. def OAI.PolycyclicRecognition.antisymmetricBarCycle line 48
  6. theorem OAI.PolycyclicRecognition.bilinearPairingChains_antisymmetric line 58
  7. def OAI.PolycyclicRecognition.bilinearPairingQuotient line 67
  8. def OAI.PolycyclicRecognition.bilinearPairingHomology line 80
  9. theorem OAI.PolycyclicRecognition.bilinearPairingHomology_π line 85
  10. theorem OAI.PolycyclicRecognition.bilinearPairingHomology_antisymmetric line 101