OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianSubgroupRank.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every abelian subgroup has bounded integral rank

An independent finite family defines an embedded integral lattice. The cohomological-dimension bound on those lattices bounds the full module rank, without assuming that the abelian subgroup is finitely generated.

  1. def OAI.PolycyclicRecognition.independentLatticeHom line 21
  2. theorem OAI.PolycyclicRecognition.independentLatticeHom_injective line 26
  3. theorem OAI.PolycyclicRecognition.abelian_subgroup_integral_rank_le line 33
  4. theorem OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension.bounds_abelian_subgroup_rank line 47