OAI/GroupTheory/PolycyclicRecognition/Lattices/JointFixedResidualNilpotent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual joint-fixed residual extension is nilpotent

The quotient need not split. Its unipotent action has finite length on every intrinsic Lie lower-central layer, and the cocycle disappears on those layers.

  1. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residual_nilpotent line 26