OAI/GroupTheory/PolycyclicRecognition/Algebra/AscendingRefinement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-index refinements of an ascending union

A finite-index subgroup of the base has uniformly bounded index at every inverse-image stage. Its increasing union therefore still has finite index. Endomorphism invariance of the base subgroup supplies invariance under the ambient automorphism.

  1. def OAI.PolycyclicRecognition.automorphismRestriction line 20
  2. theorem OAI.PolycyclicRecognition.automorphismStage_relIndex line 25
  3. theorem OAI.PolycyclicRecognition.mappedSubgroup_relIndex line 29
  4. theorem OAI.PolycyclicRecognition.mappedSubgroup_automorphism_stable line 34
  5. theorem OAI.PolycyclicRecognition.finiteIndex_automorphism_iSup_refinement line 40
  6. theorem OAI.PolycyclicRecognition.dimension_automorphism_iSup_refinement line 58