OAI/GroupTheory/PolycyclicRecognition/Analysis/HorseshoeCover.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

A projective cover adapted to a short exact coefficient sequence

The middle cover is the product of the two endpoint free covers. Its kernel will provide an exact sequence of syzygies, without claiming that the normalized free-cover functor itself is exact.

  1. theorem OAI.PolycyclicRecognition.rep_kernel_element line 18
  2. abbrev OAI.PolycyclicRecognition.horseshoeCover line 23
  3. def OAI.PolycyclicRecognition.horseshoeFst line 26
  4. def OAI.PolycyclicRecognition.horseshoeSnd line 30
  5. def OAI.PolycyclicRecognition.horseshoeInl line 34
  6. def OAI.PolycyclicRecognition.horseshoeInr line 38
  7. theorem OAI.PolycyclicRecognition.horseshoe_total line 42
  8. instance OAI.PolycyclicRecognition.horseshoeCover_projective line 51
  9. def OAI.PolycyclicRecognition.horseshoeAugmentation line 62
  10. theorem OAI.PolycyclicRecognition.horseshoeAugmentation_apply line 67
  11. theorem OAI.PolycyclicRecognition.horseshoeAugmentation_g line 73
  12. theorem OAI.PolycyclicRecognition.horseshoeInl_augmentation line 79
  13. theorem OAI.PolycyclicRecognition.horseshoeAugmentation_surjective line 90
  14. instance OAI.PolycyclicRecognition.horseshoeAugmentation_epi line 103
  15. abbrev OAI.PolycyclicRecognition.horseshoeKernel line 107
  16. def OAI.PolycyclicRecognition.horseshoeKernelInl line 110
  17. theorem OAI.PolycyclicRecognition.horseshoeKernelInl_ι line 117
  18. def OAI.PolycyclicRecognition.horseshoeKernelSnd line 121
  19. theorem OAI.PolycyclicRecognition.horseshoeKernelSnd_ι line 129
  20. theorem OAI.PolycyclicRecognition.horseshoeKernelInl_apply line 133
  21. theorem OAI.PolycyclicRecognition.horseshoeKernelSnd_apply line 139
  22. theorem OAI.PolycyclicRecognition.horseshoeKernel_condition line 145