OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteGroupRationalTelescope.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A projective telescope for rational trivial coefficients of a finite group

Consecutive free modules map by augmentation followed by the norm section, scaled by the next positive integer. The actual colimit is the rational trivial representation. Thus it has integral projective dimension at most one.

  1. abbrev OAI.PolycyclicRecognition.finiteGroupRationalStage line 20
  2. def OAI.PolycyclicRecognition.finiteGroupNormSection line 22
  3. theorem OAI.PolycyclicRecognition.finiteGroupNormSection_augmentation line 38
  4. def OAI.PolycyclicRecognition.finiteGroupRationalStep line 61
  5. def OAI.PolycyclicRecognition.finiteGroupRationalDiagram line 66
  6. def OAI.PolycyclicRecognition.finiteGroupRationalDenominator line 69
  7. theorem OAI.PolycyclicRecognition.finiteGroupRationalDenominator_ne_zero line 71
  8. theorem OAI.PolycyclicRecognition.finiteGroupRationalDenominator_succ line 76
  9. def OAI.PolycyclicRecognition.integralRationalDivision line 82
  10. def OAI.PolycyclicRecognition.finiteGroupRationalInclusion line 87
  11. theorem OAI.PolycyclicRecognition.finiteGroupRationalStep_inclusion line 92
  12. def OAI.PolycyclicRecognition.finiteGroupRationalColimit line 116
  13. theorem OAI.PolycyclicRecognition.finiteGroup_rational_projectiveDimension_le_one line 159