OAI/GroupTheory/PolycyclicRecognition/Algebra/MonicRecurrenceAscendingBase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integral action recurrences and the nilpotent finiteness endgame

A monic recurrence bounds the positive orbit of a finite generating set. Two-sided orbit generation then gives an actual finitely generated ascending base. The final theorem applies this criterion to the nilpotent abelianization; it does not assume that FP-infinity supplies the recurrence.

  1. theorem OAI.PolycyclicRecognition.ascendingBase_of_monic_recurrence line 18
  2. theorem OAI.PolycyclicRecognition.virtualSolvableFiniteDimension_of_abelianization_recurrence line 42

    Source documentation

    A finite monic certificate in the actual abelianization suffices for the already proved nilpotent-by-abelian-by-finite structural endgame.

    theorem virtualSolvableFiniteDimension_of_abelianization_recurrence
    (N : Subgroup G) [N.Normal] [Group.IsNilpotent N]
    (H : Subgroup (G ⧸ N)) [H.Normal] [H.FiniteIndex] [IsMulCommutative H]
    (t : G) (s : Finset (Abelianization N)) {d : ℕ} (hd : 0 < d) (c : Fin d → ℤ)
    (hrec : ∀ x ∈ s,
      ((characteristicQuotientAut (commutator N) (MulAut.conjNormal (H := N) t)) ^ d) x =
…

    Mentions: OAI.PolycyclicRecognition.characteristicQuotientAut