OAI/GroupTheory/PolycyclicRecognition/Algebra/PresentationKernelMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The stable kernel map of a short exact sequence

A lift of the normalized free cover of the quotient gives a map from its syzygy to the submodule. Changing the lift changes this map by a projective factor, and the construction is natural in the stable quotient.

  1. def OAI.PolycyclicRecognition.presentationKernelMapOfLift line 17
  2. theorem OAI.PolycyclicRecognition.presentationKernelMapOfLift_f line 26
  3. theorem OAI.PolycyclicRecognition.presentationKernelMapOfLift_stable_natural line 34
  4. def OAI.PolycyclicRecognition.presentationFreeLift line 63
  5. theorem OAI.PolycyclicRecognition.presentationFreeLift_g line 69
  6. def OAI.PolycyclicRecognition.presentationKernelMap line 74
  7. theorem OAI.PolycyclicRecognition.presentationKernelMap_f line 79
  8. theorem OAI.PolycyclicRecognition.presentationKernelMap_stable_natural line 84
  9. theorem OAI.PolycyclicRecognition.presentationKernelMap_f_stable_zero line 91
  10. theorem OAI.PolycyclicRecognition.presentationKernelMap_g_stable_zero line 99
  11. theorem OAI.PolycyclicRecognition.presentationKernelMap_stable_zero_of_section line 118
  12. theorem OAI.PolycyclicRecognition.presentationKernelMap_stable_inverse line 137