OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentTorsionSubgroup.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The characteristic torsion subgroup of a nilpotent group

Zero rational abelianization shows that a subgroup generated by torsion elements is torsion. This constructs the subgroup and its torsion-free quotient without a finite-generation premise.

  1. theorem OAI.PolycyclicRecognition.nilpotent_torsion_closure line 17
  2. theorem OAI.PolycyclicRecognition.nilpotent_torsion_mul line 48
  3. def OAI.PolycyclicRecognition.nilpotentTorsionSubgroup line 58
  4. theorem OAI.PolycyclicRecognition.mem_nilpotentTorsionSubgroup line 64
  5. instance OAI.PolycyclicRecognition.nilpotentTorsionSubgroup_characteristic line 67
  6. theorem OAI.PolycyclicRecognition.nilpotentTorsionQuotient_torsionFree line 76
  7. def OAI.PolycyclicRecognition.nilpotentTorsionQuotientRationalHomologyIso line 90
  8. theorem OAI.PolycyclicRecognition.finitelyGenerated_torsion_nilpotent_finite line 99
  9. theorem OAI.PolycyclicRecognition.nilpotentTorsionSubgroup_locallyFinite line 109
  10. def OAI.PolycyclicRecognition.nilpotentTorsionQuotientRationalAbelianizationEquiv line 117
  11. theorem OAI.PolycyclicRecognition.nilpotentTorsionQuotient_finiteDimension_of_finite_abelianization line 124