OAI/GroupTheory/PolycyclicRecognition/Finiteness/InducedFiniteRationalVanishing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rational vanishing for coefficients induced from finite subgroups

This is the finite-stabilizer base of the hierarchy argument. Both the projective dimension bound and the resulting complete-cohomology vanishing are proved, without a finiteness condition on the ambient group.

  1. theorem OAI.PolycyclicRecognition.finiteSubgroup_induced_rational_projectiveDimension_le_one line 19
  2. theorem OAI.PolycyclicRecognition.finiteSubgroup_induced_rational_completeCohomology line 44