OAI/GroupTheory/PolycyclicRecognition/Algebra/RegularDualPairing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Evaluation pairing with the regular dual

Inverse coefficient action makes evaluation equivariant in the regular-dual argument and invariant under the diagonal action on the other two arguments. It therefore descends to coinvariant tensor products.

  1. abbrev OAI.PolycyclicRecognition.integralModuleComm line 23
  2. def OAI.PolycyclicRecognition.integralLinearMapOfAddHom line 33
  3. def OAI.PolycyclicRecognition.regularDualEvaluation line 38
  4. theorem OAI.PolycyclicRecognition.regularDualEvaluation_apply line 52
  5. def OAI.PolycyclicRecognition.regularDualPairingInP line 56
  6. def OAI.PolycyclicRecognition.regularDualPairing line 74
  7. theorem OAI.PolycyclicRecognition.regularDualEvaluation_diagonal line 100
  8. def OAI.PolycyclicRecognition.regularTensorEvaluation line 111
  9. theorem OAI.PolycyclicRecognition.regularTensorEvaluation_invariant line 115
  10. def OAI.PolycyclicRecognition.regularCoinvariantEvaluation line 125
  11. theorem OAI.PolycyclicRecognition.regularCoinvariantEvaluation_tmul line 130