CartanSupportData.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Support data from the actual Cartan ideal

Every finite family of word bases in homogeneous lifts of an abelianization basis gives balanced positive support data. The ambient adjoint action need only be triangularizable, not diagonalizable.

def OAI.PolycyclicRecognition.cartanSupportDatum line 32
Source documentation
Support data for any finite collection of actual word bases.
```
def cartanSupportDatum {B J : Type*} [Fintype B] [Fintype J]
    (b : B → Basis J ℝ (cartanRootIdeal H))
    (words : B → J → FreeMagma (Fin m))
    (hwords : ∀ β j, evalBracketWord X (words β j) = b β j) :
    SupportDatum (HeightSpace T.character) (Fin m) B where
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.HeightSpace

theorem OAI.PolycyclicRecognition.exists_cartan_supportDatum line 54

Source documentation

In particular the support norm construction has genuine Lie algebra data for every unimodular triangular adjoint action.

theorem exists_cartan_supportDatum :
    ∃ (m : ℕ) (X : Fin m → cartanRootIdeal H) (χ : Fin m → Weight ℝ H L)
      (b : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
      (words : Fin (finrank ℝ (cartanRootIdeal H)) → FreeMagma (Fin m))
      (D : SupportDatum (HeightSpace T.character) (Fin m) Unit),
      (∀ i, (χ i).IsNonZero ∧ (X i : L) ∈ rootSpace H (χ i)) ∧
      (∀ j, evalBracketWord X (words j) = b j) ∧
      (∀ i, D.weight i = cartanHeightWeight T H (χ i)) ∧
      (∀ i, D.multiplicity () i = ∑ j, bracketWordCount (words j) i) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.cartanHeightWeight, OAI.PolycyclicRecognition.bracketWordCount