OAI/GroupTheory/PolycyclicRecognition/Algebra/LinearActionFiltration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The dimension bound for an eventually vanishing action filtration

Take successive spans of the images of a family of operators. If this descending filtration ever vanishes, it vanishes by the dimension of the space: an equality at one stage propagates to all later stages, so every nonzero stage must strictly lower dimension.

  1. def OAI.PolycyclicRecognition.linearActionStep line 18
  2. theorem OAI.PolycyclicRecognition.linearActionStep_mono line 21
  3. def OAI.PolycyclicRecognition.linearActionFiltration line 25
  4. theorem OAI.PolycyclicRecognition.linearActionFiltration_antitone line 29
  5. theorem OAI.PolycyclicRecognition.linearActionFiltration_constant line 37
  6. theorem OAI.PolycyclicRecognition.linearActionFiltration_strict_of_nonzero line 47
  7. theorem OAI.PolycyclicRecognition.linearActionFiltration_finrank_eq_bot line 58