OAI/GroupTheory/PolycyclicRecognition/Finiteness/CoarseFiniteness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coarse invariance of integral FP finiteness

The proof transfers uniform fillings and constructs finite projective covers. It does not assume homology with product coefficients or an FP recognition criterion.

  1. theorem OAI.PolycyclicRecognition.liFinitenessInput line 16
  2. theorem OAI.PolycyclicRecognition.liDualityInput line 24

    Source documentation

    Integral Poincaré duality transfers once both cohomological dimensions are finite, using the proved FP transfer and controlled cochain comparison.

    theorem liDualityInput : LiDualityInput :=
…

    Mentions: OAI.PolycyclicRecognition.LiDualityInput