OAI/GroupTheory/PolycyclicRecognition/Geometry/WordChartHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.word_length_chart_height line 17

   Source documentation

   A linear height that kills brackets scales exactly in the word-length chart. This is independent of a choice of graded limit: all nontrivial bracket words have zero height, while each letter has weight one.

   theorem word_length_chart_height
       {I L W : Type*} [Fintype I] [DecidableEq I]
       [LieRing L] [LieAlgebra ℝ L] [AddCommGroup W] [Module ℝ W]
       (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       (h : L →ₗ[ℝ] W) (hbracket : ∀ x y : L, h ⁅x, y⁆ = 0)
       {r : ℝ} (hr : 0 < r) (z : Fin (finrank ℝ L) → ℝ) :
       h ((exponentialRescaleBasis (WordBasisSelections.basis X S β)
         (fun j => (bracketWordLength (β.val j : FreeMagma I) : ℝ)) (Real.log r)).equivFun.symm z) =
         r • h ((WordBasisSelections.basis X S β).equivFun.symm z) := by
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.bracketWordLength