OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvableIntegerQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Virtual integer quotients of infinite finitely generated solvable groups

If the abelianization is finite, its kernel has finite index and one less derived step. Induction therefore finds an infinite abelian quotient in a finite-index subgroup, and a free coordinate gives the required map to ℤ.

  1. theorem OAI.PolycyclicRecognition.infinite_of_finiteIndex line 19
  2. theorem OAI.PolycyclicRecognition.virtual_integer_quotient_of_derivedSeries_eq_bot line 27
  3. theorem OAI.PolycyclicRecognition.infinite_fg_solvable_virtual_integer_quotient line 72
  4. theorem OAI.PolycyclicRecognition.infinite_fg_virtually_solvable_virtual_integer_quotient line 79