OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalOrientationExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extending the kernel orientation by its rational top homology

The conjugation action on the rationalized top homology gives an ambient character. Inverting its source gives the original integral orientation on the normal subgroup.

  1. def OAI.PolycyclicRecognition.inverseSourceRationalCharacter line 20
  2. theorem OAI.PolycyclicRecognition.exists_rationalOrientationExtension line 25