OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteResolutionTruncation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A finite resolution from finite dimension and finite generation

Canonical truncation replaces the last term by its quotient syzygy. The projectivity of that syzygy follows from finite projective dimension, while finite generation passes to the quotient.

  1. def OAI.PolycyclicRecognition.finiteResolutionShape line 18
  2. def OAI.PolycyclicRecognition.finiteResolutionEmbedding line 23
  3. instance OAI.PolycyclicRecognition.(instance at line 27) line 27
  4. theorem OAI.PolycyclicRecognition.finiteResolutionEmbedding_boundary line 33
  5. def OAI.PolycyclicRecognition.finiteTruncation line 50
  6. theorem OAI.PolycyclicRecognition.finiteTruncation_isZero line 53
  7. def OAI.PolycyclicRecognition.finiteTruncationIso line 61
  8. def OAI.PolycyclicRecognition.finiteTruncationTopIso line 66
  9. theorem OAI.PolycyclicRecognition.finiteTruncation_projective line 71
  10. theorem OAI.PolycyclicRecognition.finiteTruncation_finite line 81
  11. instance OAI.PolycyclicRecognition.finiteResolution_single_supported line 91
  12. def OAI.PolycyclicRecognition.finiteTruncationAugmentation line 100
  13. instance OAI.PolycyclicRecognition.finiteTruncationAugmentation_quasiIso line 106
  14. def OAI.PolycyclicRecognition.finiteProjectiveResolution line 115
  15. theorem OAI.PolycyclicRecognition.finiteProjectiveResolution_of_finiteDimension_typeFP line 121