OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalFiniteResolution.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The finite rational group resolution needed for the homology bound

  1. def OAI.PolycyclicRecognition.RationalResolution.resolutionOpcyclesSequence line 12
  2. theorem OAI.PolycyclicRecognition.RationalResolution.resolutionOpcyclesSequence_shortExact line 17
  3. def OAI.PolycyclicRecognition.RationalResolution.resolutionOpcyclesZeroIso line 54
  4. theorem OAI.PolycyclicRecognition.RationalResolution.resolutionOpcycles_projectiveDimension line 58
  5. theorem OAI.PolycyclicRecognition.RationalResolution.resolutionOpcycles_projective line 74
  6. def OAI.PolycyclicRecognition.RationalResolution.finiteTruncation line 82
  7. theorem OAI.PolycyclicRecognition.RationalResolution.finiteTruncation_isZero line 85
  8. def OAI.PolycyclicRecognition.RationalResolution.finiteTruncationIso line 93
  9. def OAI.PolycyclicRecognition.RationalResolution.finiteTruncationTopIso line 98
  10. theorem OAI.PolycyclicRecognition.RationalResolution.finiteTruncation_projective line 103
  11. instance OAI.PolycyclicRecognition.RationalResolution.finiteResolution_single_supported line 113
  12. def OAI.PolycyclicRecognition.RationalResolution.finiteTruncationAugmentation line 122
  13. instance OAI.PolycyclicRecognition.RationalResolution.finiteTruncationAugmentation_quasiIso line 128
  14. def OAI.PolycyclicRecognition.RationalResolution.finiteProjectiveResolution line 137
  15. theorem OAI.PolycyclicRecognition.RationalResolution.groupHomology_isZero_above_dimension line 144