OAI/GroupTheory/PolycyclicRecognition/Algebra/CommutingAscendingBases.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Combining commuting ascending actions

In a nilpotent group, two commuting automorphisms with finitely generated ascending bases have a common finitely generated invariant base. The positive orbit of one base is contained in a single stage of the other exhaustion. This avoids imposing freeness or torsion-freeness on the abelianization.

  1. theorem OAI.PolycyclicRecognition.fg_subgroup_le_automorphismStage line 18
  2. def OAI.PolycyclicRecognition.positiveOrbitSubgroup line 29
  3. theorem OAI.PolycyclicRecognition.le_positiveOrbitSubgroup line 32
  4. theorem OAI.PolycyclicRecognition.positiveOrbitSubgroup_stable line 38
  5. theorem OAI.PolycyclicRecognition.positiveOrbitSubgroup_stable_of_commute line 51
  6. theorem OAI.PolycyclicRecognition.positiveOrbitSubgroup_le line 62
  7. theorem OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase.common_base line 70
  8. theorem OAI.PolycyclicRecognition.HasFinitelyGeneratedAscendingBase.mul line 120