OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalAbelianRank.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rationalizing the bounded-rank abelian subgroups

The integral dimension bound applies even to abelian subgroups which are not finitely generated. Their rationalizations have the same rank, and the canonical map is injective because integral cohomological dimension excludes torsion. Thus these subgroups embed in finite-dimensional rational spaces.

  1. abbrev OAI.PolycyclicRecognition.RationalAbelianSpace line 24
  2. def OAI.PolycyclicRecognition.rationalAbelianMap line 26
  3. theorem OAI.PolycyclicRecognition.rationalAbelianMap_injective line 29
  4. theorem OAI.PolycyclicRecognition.rationalAbelianSpace_rank line 38
  5. theorem OAI.PolycyclicRecognition.abelian_subgroup_rational_rank_le line 42
  6. theorem OAI.PolycyclicRecognition.abelian_subgroup_rational_finite line 49
  7. theorem OAI.PolycyclicRecognition.abelian_subgroup_rationalMap_injective line 56