OAI/GroupTheory/PolycyclicRecognition/Algebra/CharacteristicFiniteIndex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Characteristic finite-index refinements

A finite-index subgroup of a finitely generated group contains a characteristic finite-index subgroup. We intersect kernels of maps into the finite permutation group on its cosets. This is the finite-index refinement needed in the induction proving virtual torsion freeness.

  1. theorem OAI.PolycyclicRecognition.finite_hom_of_finitelyGenerated line 18
  2. def OAI.PolycyclicRecognition.finiteTargetKernel line 29

    Source documentation

    The intersection only ranges over a finite type of homomorphisms.

    def finiteTargetKernel (G F : Type*) [Group G] [Group F] : Subgroup G :=
…
  3. theorem OAI.PolycyclicRecognition.finiteTargetKernel_characteristic line 32
  4. theorem OAI.PolycyclicRecognition.finiteTargetKernel_finiteIndex line 40
  5. theorem OAI.PolycyclicRecognition.exists_characteristic_finiteIndex_le line 48