OAI/GroupTheory/PolycyclicRecognition/Algebra/GroupFiniteGenerationFromFP.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

FP one implies finite generation

The finite supports of augmentation-kernel generators generate the group. Projection to the permutation module on their left cosets proves this directly.

  1. def OAI.PolycyclicRecognition.integralCosetProjection line 22
  2. theorem OAI.PolycyclicRecognition.integralCosetProjection_single line 26
  3. theorem OAI.PolycyclicRecognition.integralCosetProjection_support line 32
  4. theorem OAI.PolycyclicRecognition.mem_subgroup_of_coset_difference_zero line 51
  5. theorem OAI.PolycyclicRecognition.mem_subgroup_of_module_difference_zero line 70
  6. theorem OAI.PolycyclicRecognition.augmentationDifference_mem_kernel line 76
  7. theorem OAI.PolycyclicRecognition.group_fg_of_augmentationKernel_fg line 83
  8. theorem OAI.PolycyclicRecognition.TypeFP.fg line 115
  9. theorem OAI.PolycyclicRecognition.TypeFPInfinity.fg line 118
  10. theorem OAI.PolycyclicRecognition.HasFiniteProjectiveResolution.fg line 120