OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianizationMonoidFiniteness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The one-sided module condition in the nilpotent finiteness argument

The monoid generator acts by the inverse of conjugation. Finite generation over its integral monoid ring supplies an ascending base and hence virtual solvability and a finite cohomological dimension bound.

  1. def OAI.PolycyclicRecognition.mulAutIntegralLinear line 18
  2. def OAI.PolycyclicRecognition.inverseAutMonoidRepresentation line 21
  3. def OAI.PolycyclicRecognition.additiveMultiplicativeEquiv line 25
  4. theorem OAI.PolycyclicRecognition.ascendingBase_of_monoidModule_finite line 32
  5. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_abelianization_monoidFinite line 43