OAI/GroupTheory/PolycyclicRecognition/Algebra/BilateralDifference.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The difference operator on a bilateral direct sum

This is the algebraic calculation needed in the cyclic-extension duality argument. It applies to arbitrary coefficient modules.

  1. def OAI.PolycyclicRecognition.bilateralTranslation line 20
  2. theorem OAI.PolycyclicRecognition.bilateralTranslation_apply line 36
  3. theorem OAI.PolycyclicRecognition.bilateralTranslation_single line 39
  4. def OAI.PolycyclicRecognition.bilateralSum line 43
  5. theorem OAI.PolycyclicRecognition.bilateralSum_single line 46
  6. theorem OAI.PolycyclicRecognition.bilateralSum_translation line 49
  7. theorem OAI.PolycyclicRecognition.bilateral_sub_sum_mem_coinvariants line 56
  8. theorem OAI.PolycyclicRecognition.bilateralSum_ker line 69
  9. theorem OAI.PolycyclicRecognition.multiplicativeInt_generator line 80
  10. def OAI.PolycyclicRecognition.bilateralDifference line 86
  11. theorem OAI.PolycyclicRecognition.bilateralSum_ker_eq_range line 89
  12. theorem OAI.PolycyclicRecognition.bilateral_fixed_eq_zero line 94
  13. theorem OAI.PolycyclicRecognition.bilateralDifference_injective line 108
  14. theorem OAI.PolycyclicRecognition.bilateralSum_surjective line 114