OAI/GroupTheory/PolycyclicRecognition/Algebra/EndomorphismInvariantFiniteIndex.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Endomorphism-invariant finite-index refinements

The finite-target-kernel construction is invariant under every endomorphism, not just automorphisms. This supplies the stable torsion-free subgroup needed when passing from a virtually nilpotent base to an ascending extension.

  1. theorem OAI.PolycyclicRecognition.finiteTargetKernel_map_le line 17
  2. theorem OAI.PolycyclicRecognition.exists_endomorphismInvariant_finiteIndex_le line 24
  3. theorem OAI.PolycyclicRecognition.IsPolycyclic.exists_endomorphismInvariant_torsionFree_finiteIndex line 39