OAI/GroupTheory/PolycyclicRecognition/Lattices/ExtensionFixedCocycleSection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A section with semisimple-fixed factors in the original extension

Starting with an actual quotient lift, the semisimple centralizer still maps onto the quotient. Its moving central cocycle is removed by the constructed Lang correction, and the resulting section is returned in the original group.

  1. theorem OAI.PolycyclicRecognition.extension_exists_semisimple_fixed_cocycle_section line 22