OAI/GroupTheory/PolycyclicRecognition/Algebra/PolycyclicQuotientRank.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Lattice quotients of polycyclic groups

The already proved finite-index duality transfer gives duality for a polycyclic group of finite integral cohomological dimension. Splitting off the coordinates of a lattice quotient then bounds its rank by that dimension.

  1. theorem OAI.PolycyclicRecognition.IsPolycyclic.exists_poincareDuality_of_finiteDimension line 19
  2. theorem OAI.PolycyclicRecognition.IsPolycyclic.poincareDuality_dimension_ge_lattice_quotient line 29
  3. theorem OAI.PolycyclicRecognition.IsPolycyclic.lattice_quotient_rank_le line 63