NilpotentGenerators.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Lifting generators from the nilpotent abelianization

For the Cartan model, homogeneous lifts of a basis modulo the derived algebra generate the whole nilpotent ideal. The proof pushes the error down its actual lower central series; no generation hypothesis is substituted for this step.

theorem OAI.PolycyclicRecognition.span_sup_lowerCentralSeries_one_of_lieSpan line 18

Source documentation

Lie generation implies linear spanning modulo brackets.

theorem span_sup_lowerCentralSeries_one_of_lieSpan
    (S : Set L) (hS : LieSubalgebra.lieSpan ℝ L S = ⊤) :
    Submodule.span ℝ S ⊔ (LieModule.lowerCentralSeries ℝ L L 1).toSubmodule = ⊤ := by
…

theorem OAI.PolycyclicRecognition.lieSubalgebra_sup_lowerCentralSeries line 38

theorem OAI.PolycyclicRecognition.lieSubalgebra_eq_top_of_sup_lowerCentralSeries_one line 77

Source documentation

Lifts spanning the abelianization generate a nilpotent Lie algebra.

theorem lieSubalgebra_eq_top_of_sup_lowerCentralSeries_one
    [LieRing.IsNilpotent L] (U : LieSubalgebra ℝ L)
    (hU : U.toSubmodule ⊔ (LieModule.lowerCentralSeries ℝ L L 1).toSubmodule = ⊤) :
    U = ⊤ := by
…

theorem OAI.PolycyclicRecognition.exists_bracketWord_basis_of_abelianization line 87

Source documentation

The resulting generating family has a basis of evaluated bracket words.

theorem exists_bracketWord_basis_of_abelianization
    [LieRing.IsNilpotent L] [FiniteDimensional ℝ L]
    {I : Type*} (X : I → L)
    (hX : Submodule.span ℝ (Set.range X) ⊔
      (LieModule.lowerCentralSeries ℝ L L 1).toSubmodule = ⊤) :
    ∃ b : Module.Basis (Fin (Module.finrank ℝ L)) ℝ L,
      ∀ k, ∃ w : FreeMagma I, evalBracketWord X w = b k := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord