OAI/GroupTheory/PolycyclicRecognition/Finiteness/FreeAbelianDuality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Free abelian rank bounds from integral cohomological dimension

The coordinate homomorphism splits off one infinite cyclic quotient at a time. The resulting duality calculation bounds the rank of every embedded integral lattice in a group of finite integral cohomological dimension.

  1. abbrev OAI.PolycyclicRecognition.IntegralLatticeGroup line 18
  2. def OAI.PolycyclicRecognition.latticeCoordinate line 20
  3. def OAI.PolycyclicRecognition.latticeCoordinateSection line 25
  4. theorem OAI.PolycyclicRecognition.latticeCoordinate_section line 28
  5. def OAI.PolycyclicRecognition.latticeCoordinateKernel line 31
  6. theorem OAI.PolycyclicRecognition.integralLattice_poincareDuality line 46
  7. theorem OAI.PolycyclicRecognition.lattice_rank_le_cohomologicalDimension line 55
  8. theorem OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension.bounds_integral_lattice_rank line 63