OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalProductRepresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Gluing representations across a normal subgroup product

This is the algebraic descent used to integrate a solvable representation from its nilpotent ideal and Cartan subgroup: agreement on the intersection and compatibility with conjugation are exactly the required relations.

  1. theorem OAI.PolycyclicRecognition.exists_representation_of_factor_maps line 19