OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalSubgroupFiltration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pulling the rational action filtration back to the group

The rational filtration on an abelian normal subgroup gives actual ambient subgroups. Commuting with the ambient group advances the filtration. Its last term is trivial when the abelian subgroup is torsion free.

  1. def OAI.PolycyclicRecognition.rationalPreimageSubgroup line 20
  2. def OAI.PolycyclicRecognition.rationalSubgroupFiltration line 35
  3. theorem OAI.PolycyclicRecognition.rationalSubgroupFiltration_zero line 39
  4. theorem OAI.PolycyclicRecognition.rationalAbelianMap_conjugationDifference line 44
  5. theorem OAI.PolycyclicRecognition.rationalSubgroupFiltration_commutator line 50
  6. theorem OAI.PolycyclicRecognition.rationalSubgroupFiltration_eq_bot line 68
  7. theorem OAI.PolycyclicRecognition.lowerCentralSeries_le_rationalSubgroupFiltration line 79