OAI/GroupTheory/PolycyclicRecognition/Finiteness/LocalInductionVanishing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Vanishing for locally controlled height-kernel coefficients

Only finite projective dimension at each finitely generated subgroup is used; there is no uniform bound on those dimensions. In particular this applies to locally finite kernels, and to torsion-free locally nilpotent kernels.

  1. theorem OAI.PolycyclicRecognition.TypeFPInfinity.induction_locally_finite_dimension_vanishing line 22
  2. theorem OAI.PolycyclicRecognition.TypeFPInfinity.locallyFinite_smallCoefficient_induction_vanishing line 44
  3. theorem OAI.PolycyclicRecognition.TypeFPInfinity.locallyNilpotent_smallCoefficient_induction_vanishing line 55