OAI/GroupTheory/PolycyclicRecognition/Finiteness/NilpotentLatticeDuality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The dimension reduction in nilpotent-by-abelian duality

The ambient duality dimension is bounded by the sum of the kernel dimension and the lattice rank. Equality yields finite generation through integral orientation homology.

  1. theorem OAI.PolycyclicRecognition.nilpotent_lattice_duality_degree line 21