CartanWordBasis.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A homogeneous bracket-word basis of the Cartan ideal

This supplies actual nonzero-root letters and strictly positive integral letter multiplicities for the nilpotent box data.

def OAI.PolycyclicRecognition.cartanGeneratorPool line 23
theorem OAI.PolycyclicRecognition.cartanGeneratorPool_lieSpan line 26
abbrev OAI.PolycyclicRecognition.cartanRootAbelianization line 54

theorem OAI.PolycyclicRecognition.exists_cartan_abelianization_generators line 60

Source documentation

Retain the actual abelianization basis along with its homogeneous lifts. This gives positivity for every later choice of a word basis.

theorem exists_cartan_abelianization_generators [FiniteDimensional ℝ L]
    {n : ℕ} (T : TriangularAdjoint L n) :
    ∃ (m : ℕ) (X : Fin m → cartanRootIdeal H) (χ : Fin m → Weight ℝ H L)
      (b : Basis (Fin m) ℝ (cartanRootAbelianization H)),
      (∀ i, (χ i).IsNonZero ∧ (X i : L) ∈ rootSpace H (χ i)) ∧
      (∀ i, (LieModule.lowerCentralSeries ℝ (cartanRootIdeal H)
        (cartanRootIdeal H) 1).toSubmodule.mkQ (X i) = b i) ∧
      LieSubalgebra.lieSpan ℝ (cartanRootIdeal H) (Set.range X) = ⊤ := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanRootAbelianization

theorem OAI.PolycyclicRecognition.exists_cartan_word_basis line 83

Source documentation

The actual Cartan ideal has a basis of bracket words in finitely many nonzero generalized root vectors, with every letter occurring positively.

theorem exists_cartan_word_basis [FiniteDimensional ℝ L]
    {n : ℕ} (T : TriangularAdjoint L n) :
    ∃ (m : ℕ) (X : Fin m → cartanRootIdeal H) (χ : Fin m → Weight ℝ H L)
      (b : Basis (Fin (Module.finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
      (words : Fin (Module.finrank ℝ (cartanRootIdeal H)) → FreeMagma (Fin m)),
      (∀ i, (χ i).IsNonZero ∧ (X i : L) ∈ rootSpace H (χ i)) ∧
      (∀ j, evalBracketWord X (words j) = b j) ∧
      (∀ i, 0 < ∑ j, bracketWordCount (words j) i) := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordCount

theorem OAI.PolycyclicRecognition.cartan_generator_weights_separate line 99

Source documentation

The weights of a generating family in the Cartan ideal already separate canonical height; one need not retain the full set of adjoint weights.

theorem cartan_generator_weights_separate [FiniteDimensional ℝ L]
    {n : ℕ} (T : TriangularAdjoint L n) {I : Type*}
    (X : I → cartanRootIdeal H) (χ : I → Weight ℝ H L)
    (hX : ∀ i, (X i : L) ∈ rootSpace H (χ i))
    (hgen : LieSubalgebra.lieSpan ℝ (cartanRootIdeal H) (Set.range X) = ⊤)
    (w : HeightSpace T.character)
    (hw : ∀ i, cartanHeightWeight T H (χ i) w = 0) : w = 0 := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.cartanHeightWeight