OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalExteriorHomology.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational second homology surjects onto the rational exterior square

  1. def OAI.PolycyclicRecognition.rationalUnit line 15
  2. theorem OAI.PolycyclicRecognition.rationalUnit_span line 18
  3. def OAI.PolycyclicRecognition.rationalExteriorValue line 33
  4. theorem OAI.PolycyclicRecognition.rationalExteriorValue_swap line 36
  5. theorem OAI.PolycyclicRecognition.rationalExteriorValue_add_left line 46
  6. def OAI.PolycyclicRecognition.rationalIntegralWedgePairing line 51
  7. def OAI.PolycyclicRecognition.rationalLinearExtension line 77
  8. theorem OAI.PolycyclicRecognition.rationalLinearExtension_tmul line 82
  9. def OAI.PolycyclicRecognition.rationalAbelianH2Exterior line 87
  10. theorem OAI.PolycyclicRecognition.rationalAbelianH2Exterior_class line 92
  11. theorem OAI.PolycyclicRecognition.rationalAbelianH2Exterior_surjective line 108
  12. theorem OAI.PolycyclicRecognition.rationalAbelianH2Exterior_natural line 127