OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteKernelAscendingBase.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Lifting an ascending base across a finite kernel

Finite kernels preserve the concrete ascending-base property. They also preserve virtual nilpotence: intersect with the centralizer of the finite kernel, then use the central-extension criterion for nilpotence.

  1. theorem OAI.PolycyclicRecognition.fg_preimage_of_finite_kernel line 18
  2. theorem OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase.of_finite_kernel line 39
  3. theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_finite_kernel line 57
  4. theorem OAI.PolycyclicRecognition.virtuallyNilpotent_preimage_of_finite_kernel line 71
  5. theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_finiteIndex line 87
  6. theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_finite_kernel_of_virtuallyNilpotent line 100
  7. theorem OAI.PolycyclicRecognition.virtuallyNilpotent_preimage_of_finite_kernel_of_virtuallyNilpotent line 108