OAI/GroupTheory/PolycyclicRecognition/Algebra/OneSidedOrbitAscendingBase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

One-sided orbit generation and finite ascending bases

For an abelian kernel this is the concrete group form of finite generation over the monoid ring in the contracting direction. A finite positive-orbit bound constructs the base; it is not assumed.

  1. theorem OAI.PolycyclicRecognition.finiteOrbitSubgroup_monotone line 16
  2. theorem OAI.PolycyclicRecognition.iSup_finiteOrbitSubgroup line 24
  3. theorem OAI.PolycyclicRecognition.finiteOrbitSubgroup_inverse_stable line 37
  4. theorem OAI.PolycyclicRecognition.ascendingBase_of_oneSided_orbit line 59
  5. theorem OAI.PolycyclicRecognition.ascendingBase_iff_oneSided_orbit line 87