OAI/GroupTheory/PolycyclicRecognition/Analysis/ExteriorShiftIntegrality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial relations for shifts on finite exterior modules

For an abelian acting group, applying a scalar shift of a group operator in every exterior coordinate commutes with the diagonal action. If the exterior module is finite, this operator satisfies a monic polynomial over the group ring.

  1. def OAI.PolycyclicRecognition.exteriorShift line 18
  2. theorem OAI.PolycyclicRecognition.exteriorShift_intertwines line 22
  3. def OAI.PolycyclicRecognition.exteriorShiftIntertwining line 41
  4. def OAI.PolycyclicRecognition.exteriorShiftModule line 46
  5. theorem OAI.PolycyclicRecognition.exteriorShiftModule_integral line 55
  6. theorem OAI.PolycyclicRecognition.exteriorShiftModule_monic_relation line 62