FiniteWordBases.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

All bases from a finite word list

The indexing type is finite and includes every ordered word basis selected from the list. Nilpotence proves this family is nonempty for a generating alphabet, including the zero-dimensional case.

def OAI.PolycyclicRecognition.WordBasisSelections line 21
Source documentation
All ordered bases selected from S, retaining the actual word labels.
```
def WordBasisSelections (X : I → L) (S : Finset (FreeMagma I)) :=
…
```
instance OAI.PolycyclicRecognition.WordBasisSelections.(instance at line 29) line 29
def OAI.PolycyclicRecognition.WordBasisSelections.words line 35
Source documentation
The word labels of this selected basis.
```
def words (β : WordBasisSelections X S) (j : Fin (finrank ℝ L)) : FreeMagma I := β.val j
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections
def OAI.PolycyclicRecognition.WordBasisSelections.basis line 38
Source documentation
The corresponding actual basis of the Lie algebra.
```
def basis (β : WordBasisSelections X S) : Basis (Fin (finrank ℝ L)) ℝ L :=
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections
theorem OAI.PolycyclicRecognition.WordBasisSelections.eval_words line 41
theorem OAI.PolycyclicRecognition.WordBasisSelections.words_mem line 45
theorem OAI.PolycyclicRecognition.nonempty_wordBasisSelections line 54
Source documentation
A basis chosen from all words automatically belongs to the finite list: any omitted word is zero and therefore cannot be a basis vector.
```
theorem nonempty_wordBasisSelections (X : I → L) {k : ℕ}
    (hk : lowerCentralSeries ℝ L L k = ⊥)
    (hgen : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤) :
    Nonempty (WordBasisSelections X (boundedBracketWords k)) := by
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.boundedBracketWords