OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicSchreierKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual kernel of an infinite cyclic quotient is finitely generated

Schreier corrections of the given generators, and all their cyclic conjugates, generate the kernel. Polynomial growth makes this a finite window.

  1. theorem OAI.PolycyclicRecognition.cyclicConjugateSubgroup_conjugation line 16
  2. def OAI.PolycyclicRecognition.cyclicSchreierLetter line 30
  3. theorem OAI.PolycyclicRecognition.cyclicHeight_zpow line 34
  4. theorem OAI.PolycyclicRecognition.cyclicSchreierLetter_mem_ker line 42
  5. theorem OAI.PolycyclicRecognition.cyclicSchreierKernel_eq line 50
  6. theorem OAI.PolycyclicRecognition.cyclic_kernel_fg_of_polynomial_growth line 99