OAI/GroupTheory/PolycyclicRecognition/Algebra/RegularDualRepresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The contravariant regular dual of a group-ring representation

The regular dual is Hom over the group ring into the regular module, with left action induced by inverse right translation on the target. This is the representation used in the top-degree duality pairing.

  1. def OAI.PolycyclicRecognition.regularRightTranslation line 21
  2. theorem OAI.PolycyclicRecognition.regularRightTranslation_single line 24
  3. theorem OAI.PolycyclicRecognition.regularRightTranslation_one line 31
  4. theorem OAI.PolycyclicRecognition.regularRightTranslation_mul line 42
  5. def OAI.PolycyclicRecognition.regularDualRepresentation line 57
  6. def OAI.PolycyclicRecognition.regularDual line 72
  7. def OAI.PolycyclicRecognition.regularDualMap line 74
  8. theorem OAI.PolycyclicRecognition.regularDualMap_apply line 81