OAI/GroupTheory/PolycyclicRecognition/Lattices/JointFixedReductionData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Constructed joint-fixed residual data for an actual extension

The residual group is defined by the actual section factors and embeds in the original extension. The prescribed quotient lifts act unipotently on its kernel Lie algebra.

  1. structure OAI.PolycyclicRecognition.JointFixedReductionData line 22
  2. theorem OAI.PolycyclicRecognition.exists_jointFixedReductionData line 37
  3. def OAI.PolycyclicRecognition.JointFixedReductionData.action line 49
  4. theorem OAI.PolycyclicRecognition.JointFixedReductionData.action_commutes line 53
  5. def OAI.PolycyclicRecognition.JointFixedReductionData.residualSystem line 57
  6. def OAI.PolycyclicRecognition.JointFixedReductionData.residualEmbedding line 62
  7. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residualEmbedding_injective line 68
  8. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residual_generator_unipotent line 74
  9. theorem OAI.PolycyclicRecognition.JointFixedReductionData.residual_kernel_nilpotent line 81