OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteOrbitAscendingBase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit bounds produce an ascending base

This is the group-theoretic bridge from a monic action relation to the ascending-base condition used in the elementary-amenable finiteness argument. No finite generation of the whole kernel is required.

  1. def OAI.PolycyclicRecognition.finiteOrbitSubgroup line 16
  2. theorem OAI.PolycyclicRecognition.finiteOrbitSubgroup_fg line 19
  3. theorem OAI.PolycyclicRecognition.le_finiteOrbitSubgroup line 23
  4. theorem OAI.PolycyclicRecognition.finiteOrbitSubgroup_stable line 29
  5. theorem OAI.PolycyclicRecognition.automorphism_exhaustion_of_integer_orbits line 46
  6. theorem OAI.PolycyclicRecognition.ascendingBase_of_finite_orbit_relation line 72