OAI/GroupTheory/PolycyclicRecognition/Finiteness/InductionExhaustionVanishing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complete vanishing for induction along a subgroup exhaustion

The finite stages may have arbitrarily large projective dimensions. The ambient group's FP-infinity hypothesis supplies continuity of its completed cohomology for the actual induced-coefficient colimit.

  1. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.transportIso line 21
  2. def OAI.PolycyclicRecognition.inducedExhaustionDiagram line 43
  3. def OAI.PolycyclicRecognition.inducedExhaustionColimit line 49
  4. theorem OAI.PolycyclicRecognition.TypeFPInfinity.induction_exhaustion_complete_vanishing line 63