OAI/GroupTheory/PolycyclicRecognition/Algebra/ActionDepth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Commutators advance an operator filtration

If every action difference raises a descending filtration by one step, its commutators raise it further. This controls the lower central series using the length at which the action filtration vanishes.

  1. def OAI.PolycyclicRecognition.ActionDepth line 20
  2. theorem OAI.PolycyclicRecognition.ActionDepth.zero line 27
  3. theorem OAI.PolycyclicRecognition.ActionDepth.mono line 29
  4. theorem OAI.PolycyclicRecognition.ActionDepth.add line 33
  5. theorem OAI.PolycyclicRecognition.ActionDepth.neg line 37
  6. theorem OAI.PolycyclicRecognition.ActionDepth.sub line 40
  7. theorem OAI.PolycyclicRecognition.ActionDepth.mul line 43
  8. theorem OAI.PolycyclicRecognition.ActionDepth.one line 48
  9. theorem OAI.PolycyclicRecognition.ActionDepth.generator line 52
  10. theorem OAI.PolycyclicRecognition.ActionDepth.eq_zero line 56
  11. theorem OAI.PolycyclicRecognition.lowerCentralSeries_le_ker_of_actionFiltration line 67