OAI/GroupTheory/PolycyclicRecognition/Finiteness/LiDualityFromFiniteness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Deriving the duality transfer from finiteness transfer

The cohomology comparison is proved by controlled cochains. Canonical truncation supplies a finite projective resolution once FP infinity and finite cohomological dimension are known. Thus the application of Li, Corollary 4.48, requires no independent hypothesis beyond the Corollary 4.47 finiteness transfer.

  1. theorem OAI.PolycyclicRecognition.liDualityInput_of_finiteness line 17