OAI/GroupTheory/PolycyclicRecognition/Geometry/LieWordDifferential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Differentials of bracket words and the lower central series

Changing the basepoint in the differential of a Lie polynomial changes its linear part only by a map that raises the lower central series. This is the algebraic part of the Jacobian computation for nilpotent exponential coordinates.

  1. def OAI.PolycyclicRecognition.rightBracketLinear line 22
  2. def OAI.PolycyclicRecognition.bracketWordDifferential line 27
  3. theorem OAI.PolycyclicRecognition.bracketWordDifferential_of line 33
  4. theorem OAI.PolycyclicRecognition.bracketWordDifferential_mul line 36
  5. theorem OAI.PolycyclicRecognition.bracketWordDifferential_mem line 42
  6. theorem OAI.PolycyclicRecognition.bracketWordDifferential_mul_mem_succ line 50
  7. theorem OAI.PolycyclicRecognition.bracketWordDifferential_sub_mem_succ line 69
  8. def OAI.PolycyclicRecognition.finiteDynkinDifferential line 82
  9. theorem OAI.PolycyclicRecognition.finiteDynkinDifferential_sub_mem_succ line 87