OAI/GroupTheory/PolycyclicRecognition/Algebra/InvariantTopTwist.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Making rank-one top homology invariant by a scalar twist

The twist is trivial on the normal subgroup. Its character is obtained from actual conjugation on rationalized homology, so no orientation extension is assumed for an intermediate subgroup of a lattice quotient.

  1. theorem OAI.PolycyclicRecognition.exists_invariantTopTwist line 21