Lower-central weights and adapted bases

Write C k = LieModule.lowerCentralSeries R L L k, so C 0 = L and C 1 = [L,L]. The bracket satisfies [C m, C n] ≤ C (m + n + 1). Thus a vector in C (w - 1) has lower-central weight at least w, and brackets add these positive weights.

For a finite-dimensional nilpotent Lie algebra, exists_basis_weight_lowerCentralSeries supplies a finite ordered basis with positive bounded weights, describing every term of the lower central series by coordinate vanishing. In particular, a bracket of basis vectors has no coordinate of weight less than the sum of their weights. This is the weight bound needed to straighten PBW monomials without lowering weight, and to construct finite weighted enveloping-algebra quotients. No characteristic or algebraic-closure hypothesis is used.

References

• N. Jacobson, Lie Algebras, Interscience (1962), Chapters II and V, for the lower central series, nilpotent Lie algebras and universal enveloping algebras.

theorem TauCeti.lie_lowerCentralSeries_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (m n : ℕ) : ⁅LieModule.lowerCentralSeries R L L m, LieModule.lowerCentralSeries R L M n⁆ ≤ LieModule.lowerCentralSeries R L M (m + n + 1)

Brackets add lower-central weights. The zero-indexed convention C 0 = L accounts for the extra 1 in the index on the right.

theorem Module.Basis.repr_lie_eq_zero_of_weight_lt {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {ι : Type u_3} (b : Basis ι R L) (w : ι → ℕ) (hpos : ∀ (i : ι), 0 < w i) (hmem : ∀ (k : ℕ) (x : L), x ∈ LieModule.lowerCentralSeries R L L k ↔ ∀ (i : ι), w i ≤ k → (b.repr x) i = 0) (i j k : ι) (hk : w k < w i + w j) : (b.repr ⁅b i, b j⁆) k = 0

A bracket has zero coordinates below the sum of the weights of its two inputs in a basis adapted to the lower central series.

theorem TauCeti.exists_basis_weight_lowerCentralSeries {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieRing.IsNilpotent L] : ∃ (N : ℕ) (b : Module.Basis (Fin (Module.finrank K L)) K L) (w : Fin (Module.finrank K L) → ℕ), (∀ (i : Fin (Module.finrank K L)), 0 < w i ∧ w i ≤ N) ∧ (∀ (k : ℕ) (x : L), x ∈ LieModule.lowerCentralSeries K L L k ↔ ∀ (i : Fin (Module.finrank K L)), w i ≤ k → (b.repr x) i = 0) ∧ ∀ (i j k : Fin (Module.finrank K L)), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0

Every finite-dimensional nilpotent Lie algebra has a finite ordered basis with positive bounded lower-central weights. Each central-series term is described exactly by coordinate vanishing, and brackets of basis vectors have no coordinates below the sum of their weights.