OAI/GroupTheory/PolycyclicRecognition/Finiteness/SequentialProjectiveTelescope.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A length-one projective resolution of a sequential projective colimit

The differential is identity minus the forward shift. Its injectivity uses induction on coordinates, and the cokernel is the given concrete colimit.

  1. abbrev OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeSum line 21
  2. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeShift line 23
  3. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeDifferential line 27
  4. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeShift_inclusion line 30
  5. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeShift_zero line 39
  6. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeShift_succ line 53
  7. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.telescopeDifferential_injective line 73
  8. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeAugmentation line 94
  9. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeDifferential_augmentation line 97
  10. instance OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeAugmentation_epi line 106
  11. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeSequence line 114
  12. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeCokernelCompatible line 118
  13. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeCokernelDescent line 144
  14. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeAugmentation_cokernelDescent line 148
  15. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.telescopeSequence_shortExact line 159
  16. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.projectiveDimension_le_one line 175