BracketWords.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Actual bracket words for the nilpotent box construction

The linear span of evaluated bracket words is exactly the generated Lie subalgebra. A finite-dimensional generated algebra therefore has a basis chosen from actual words. Letter counts give the weights of these words, including for generalized weight vectors.

def OAI.PolycyclicRecognition.evalBracketWord line 26
theorem OAI.PolycyclicRecognition.evalBracketWord_of line 31
theorem OAI.PolycyclicRecognition.evalBracketWord_mul line 35
def OAI.PolycyclicRecognition.bracketWordCount line 38
theorem OAI.PolycyclicRecognition.evalBracketWord_mem_lieSpan line 42
theorem OAI.PolycyclicRecognition.evalBracketWord_map line 48
theorem OAI.PolycyclicRecognition.span_evalBracketWord line 55
theorem OAI.PolycyclicRecognition.exists_bracketWord_basis line 91
Source documentation
No abstract choice of a spanning vector is needed: every selected basis vector is the evaluation of a bracket word in the supplied generators.
```
theorem exists_bracketWord_basis [FiniteDimensional ℝ L] (X : I → L)
    (hX : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤) :
    ∃ b : Basis (Fin (Module.finrank ℝ L)) ℝ L,
      ∀ k, ∃ w : FreeMagma I, evalBracketWord X w = b k := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord
def OAI.PolycyclicRecognition.bracketWordWeight line 108
theorem OAI.PolycyclicRecognition.bracketWordWeight_eq_count line 113

theorem OAI.PolycyclicRecognition.evalBracketWord_mem_generalizedWeight line 125

Source documentation

Generalized weight vectors remain generalized after taking brackets. The nilpotent part of the Cartan action is retained.

theorem evalBracketWord_mem_generalizedWeight
    (H : LieSubalgebra ℝ L) (α : I → H →ₗ[ℝ] ℝ) (X : I → L)
    (hX : ∀ i (h : H), X i ∈ (LieAlgebra.ad ℝ L h).maxGenEigenspace (α i h))
    (w : FreeMagma I) (h : H) :
    evalBracketWord X w ∈
      (LieAlgebra.ad ℝ L h).maxGenEigenspace (bracketWordWeight α w h) := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordWeight