OAI/GroupTheory/PolycyclicRecognition/Finiteness/CoarsePoincareDuality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cohomological part of Poincare duality transfer

Coarse invariance supplies the vanishing and the integral top class. Existence of a finite projective resolution is a separate algebraic finiteness obligation.

  1. theorem OAI.PolycyclicRecognition.poincareDuality_of_coarse_finiteResolution line 16