OAI/GroupTheory/PolycyclicRecognition/Lattices/JointFixedLayerAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The abelian quotient acts on the residual lower-central layers

Inner section factors disappear on these layers, so this is an actual linear representation of the quotient. Its selected generators are unipotent.

  1. abbrev OAI.PolycyclicRecognition.JointFixedReductionData.lowerCentralLayer line 27
  2. def OAI.PolycyclicRecognition.JointFixedReductionData.layerEnd line 31
  3. def OAI.PolycyclicRecognition.JointFixedReductionData.layerAction line 39
  4. theorem OAI.PolycyclicRecognition.JointFixedReductionData.layer_generator_unipotent line 70
  5. theorem OAI.PolycyclicRecognition.JointFixedReductionData.layer_action_filtration line 80