OAI/GroupTheory/PolycyclicRecognition/Algebra/WordLengthFiltration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Word-length filtration for a nilpotent generated algebra

Left multiplication raises word length; a derivation carrying generators to generators preserves it. This separates the nilpotent and semisimple parts of the finite solvable representation.

  1. def OAI.PolycyclicRecognition.wordLengthSpan line 18
  2. theorem OAI.PolycyclicRecognition.wordLengthSpan_antitone line 21
  3. theorem OAI.PolycyclicRecognition.wordLengthSpan_generator_mul line 27
  4. theorem OAI.PolycyclicRecognition.wordLengthSpan_zero_eq_top line 42
  5. theorem OAI.PolycyclicRecognition.wordLengthSpan_eq_bot line 64
  6. theorem OAI.PolycyclicRecognition.wordLengthSpan_prefix_derivative line 78
  7. theorem OAI.PolycyclicRecognition.wordLengthSpan_derivative line 97