OAI/GroupTheory/PolycyclicRecognition/Algebra/ExhaustionOrientationDetection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Detecting the orientation by nonzero top homology

A nonzero class survives in every sufficiently large stage of an exhaustion. For rank-one integral coefficients, top duality at those stages identifies the coefficient representation with the compatible orientation.

  1. theorem OAI.PolycyclicRecognition.exhaustion_orientation_of_nonzero_top line 21