NilpotentBasisWordChoices.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite word choices for the actual Cartan basis

theorem OAI.PolycyclicRecognition.exists_nilpotent_basis_word_choices line 18

Source documentation

A fixed linear basis supplies a finite generating alphabet. Nilpotence and finite maximization supply all remaining word-chart choices.

theorem exists_nilpotent_basis_word_choices (b : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ (d : ℕ) (β : WordBasisSelections (fun i => b i) (boundedBracketWords d)),
      lowerCentralSeries ℝ L L d = ⊥ ∧
      (∀ i : Fin (finrank ℝ L), FreeMagma.of i ∈ boundedBracketWords d) ∧
      IsMaximizingColumnBasis (wordListCoordinates (fun i => b i) (boundedBracketWords d) b)
        (fun w => bracketWordExponent (fun _ : Fin (finrank ℝ L) => 1) w) β.val := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent