OAI/GroupTheory/PolycyclicRecognition/Finiteness/ScalarHigherHomologyExterior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Higher rational homology maps onto exterior powers

The map is built on the actual bar complex. Signed permutation cycles give preimages of pure wedges after division by the factorial of the degree.

  1. def OAI.PolycyclicRecognition.scalarIntegralExterior line 18
  2. theorem OAI.PolycyclicRecognition.scalarIntegralExterior_apply line 27
  3. def OAI.PolycyclicRecognition.scalarHomologyExterior line 31
  4. theorem OAI.PolycyclicRecognition.scalarHomologyExterior_class line 37
  5. theorem OAI.PolycyclicRecognition.scalarTensorUnit_span line 46
  6. theorem OAI.PolycyclicRecognition.scalarHomologyExterior_surjective_of_factorial_ne_zero line 59
  7. theorem OAI.PolycyclicRecognition.scalarHomologyExterior_surjective line 79