OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteIndexOrientation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of top-homology orientations at finite index

A nonzero intertwiner between integral rank-one representations determines their isomorphism. Shapiro and finite-index induction/coinduction produce that intertwiner without choosing fundamental classes.

  1. theorem OAI.PolycyclicRecognition.topHomology_orientation_restrict line 24
  2. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.topHomology_orientation_finiteIndex line 50