OAI/GroupTheory/PolycyclicRecognition/Finiteness/ReducedCohomologyDescent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Descent of compact coboundary approximations along a group quotient

Compact lifts suffice. Injectivity and compactness of the kernel are not needed, which is essential for the overlapping Cartan factor map.

  1. theorem OAI.PolycyclicRecognition.UnitaryReducedVanishing.of_surjective_compact_lifts line 19