OAI/GroupTheory/PolycyclicRecognition/Algebra/ScalarExtendedH2CrossProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The second-homology cross product over a field

Both variables of the integral cross product are extended by scalars. Its alternation is proved directly, including in characteristic two.

  1. def OAI.PolycyclicRecognition.scalarTensorUnit line 18
  2. def OAI.PolycyclicRecognition.scalarExtensionLinear line 21
  3. theorem OAI.PolycyclicRecognition.scalarExtensionLinear_tmul line 25
  4. def OAI.PolycyclicRecognition.scalarExtensionOperator line 29
  5. def OAI.PolycyclicRecognition.abelianH2Bilinear line 45
  6. def OAI.PolycyclicRecognition.scalarH2PairingIntegral line 59
  7. def OAI.PolycyclicRecognition.scalarExtendedH2Pairing line 78
  8. theorem OAI.PolycyclicRecognition.scalarExtendedH2Pairing_tmul line 83
  9. theorem OAI.PolycyclicRecognition.scalarExtendedH2Pairing_swap line 89
  10. theorem OAI.PolycyclicRecognition.scalarExtendedH2Pairing_self line 104
  11. def OAI.PolycyclicRecognition.scalarExtendedH2Alternating line 112
  12. def OAI.PolycyclicRecognition.scalarExtendedH2ExteriorProduct line 127
  13. theorem OAI.PolycyclicRecognition.scalarExtendedH2ExteriorProduct_value line 132