Brackets in the extension of scalars of a perfect Lie algebra

Let L be a perfect Lie algebra over R, that is ⁅L, L⁆ = L, and let A be a commutative R-algebra. In the extension of scalars A ⊗[R] L, every tensor (a * b) ⊗ x is an R-linear combination of brackets ⁅a ⊗ y, b ⊗ z⁆, because x is a combination of brackets ⁅y, z⁆ and ⁅a ⊗ y, b ⊗ z⁆ = (a * b) ⊗ ⁅y, z⁆. The coefficient factorization a * b is arbitrary, which is what lets loop and current algebras split a mode or a current of high order into brackets of modes or currents of lower order.

Main results

• TauCeti.LieAlgebra.mem_span_lie_of_derivedSeries_one_eq_top: a perfect Lie algebra is the R-span of its brackets; TauCeti.LieAlgebra.derivedSeries_one_eq_top_of_le_span_lie is the converse.
• TauCeti.LieAlgebra.ExtendScalars.mul_tmul_mem_span_lie: for perfect L, (a * b) ⊗ x lies in the R-span of the brackets ⁅a ⊗ y, b ⊗ z⁆.

theorem TauCeti.LieAlgebra.mem_span_lie_of_derivedSeries_one_eq_top {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] (hL : LieAlgebra.derivedSeries R L 1 = ⊤) (x : L) : x ∈ Submodule.span R {x : L | ∃ (y : L) (z : L), ⁅y, z⁆ = x}

A perfect Lie algebra is spanned by its brackets: if ⁅L, L⁆ = L, then every element of L is an R-linear combination of brackets ⁅y, z⁆.

theorem TauCeti.LieAlgebra.derivedSeries_one_eq_top_of_le_span_lie {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] (h : ⊤ ≤ Submodule.span R {x : L | ∃ (y : L) (z : L), ⁅y, z⁆ = x}) : LieAlgebra.derivedSeries R L 1 = ⊤

A Lie algebra spanned by its brackets is perfect: the converse of mem_span_lie_of_derivedSeries_one_eq_top.

theorem TauCeti.LieAlgebra.ExtendScalars.mul_tmul_mem_span_lie {R : Type u_1} {A : Type u_2} {L : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] (hL : LieAlgebra.derivedSeries R L 1 = ⊤) (a b : A) (x : L) : (a * b) ⊗ₜ[R] x ∈ Submodule.span R {u : TensorProduct R A L | ∃ (y : L) (z : L), ⁅a ⊗ₜ[R] y, b ⊗ₜ[R] z⁆ = u}

Tensors over a perfect Lie algebra are sums of brackets with prescribed coefficients. If L is perfect, then for all coefficients a and b every tensor (a * b) ⊗ x is an R-linear combination of brackets ⁅a ⊗ y, b ⊗ z⁆.