OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalFiniteIndexHomology.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rational surjectivity from a finite-index subgroup

The actual Shapiro transfer followed by inclusion is multiplication by the subgroup index. Rationalization therefore makes inclusion surjective in every degree, with arbitrary coefficients restricted from the ambient group.

  1. theorem OAI.PolycyclicRecognition.homology_map_nsmul_identity line 20
  2. def OAI.PolycyclicRecognition.finiteIndexHomologyTransfer line 44
  3. theorem OAI.PolycyclicRecognition.finiteIndexHomologyTransfer_inclusion line 50
  4. theorem OAI.PolycyclicRecognition.rational_finiteIndex_homology_surjective line 58
  5. theorem OAI.PolycyclicRecognition.rational_nestedSubgroup_homology_surjective line 89