OAI/GroupTheory/PolycyclicRecognition/Algebra/ActionWordFiltration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Operator words and the action filtration

The image-span filtration is controlled by products of the operators. This turns any uniform vanishing length into the dimension bound proved for that filtration.

  1. def OAI.PolycyclicRecognition.actionOperatorWord line 17
  2. theorem OAI.PolycyclicRecognition.linearActionFiltration_le_ker line 20
  3. theorem OAI.PolycyclicRecognition.linearActionFiltration_eq_bot_of_word_zero line 39
  4. theorem OAI.PolycyclicRecognition.actionOperatorWord_apply_mem line 47
  5. theorem OAI.PolycyclicRecognition.actionOperatorWord_zero_of_filtration_eq_bot line 58
  6. theorem OAI.PolycyclicRecognition.actionOperatorWord_zero_at_finrank line 67