OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicJoinDimension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Adjoining a lift of an infinite cyclic quotient

If the lift normalizes a subgroup of the kernel, its join with that subgroup has precisely the expected kernel. This gives the dimension and solvability bounds without imposing normality in the whole ambient group.

  1. theorem OAI.PolycyclicRecognition.cyclicJoin_kernel_le line 24
  2. def OAI.PolycyclicRecognition.cyclicJoinKernelMap line 42
  3. theorem OAI.PolycyclicRecognition.cyclicJoinKernelMap_injective line 49
  4. theorem OAI.PolycyclicRecognition.cyclicJoin_finiteDimension line 56
  5. theorem OAI.PolycyclicRecognition.cyclicJoin_solvable line 72