OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentLatticeInnerAction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unipotent corrections in a nonsplit nilpotent-by-abelian extension

Commutators of quotient lifts need not be trivial. Their induced action on the nilpotent Lie model is the actual inner action and is unipotent.

  1. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLinear_inner_unipotent line 20
  2. def OAI.PolycyclicRecognition.nilpotentConjugationLinear line 38
  3. theorem OAI.PolycyclicRecognition.nilpotentConjugationLinear_inner_unipotent line 41
  4. theorem OAI.PolycyclicRecognition.nilpotentConjugationLinear_commutator_unipotent line 47