Levi decomposition

TheoremWeyl's complete reducibility theorem#✓fully proved

Let \(L\) be a finite-dimensional semisimple Lie algebra over a field \(K\) of characteristic zero, and let \(M\) be a finite-dimensional Lie module over \(L\) and \(K\). Then every Lie submodule \(W\) of \(M\) has a complement: there is a Lie submodule \(U\) of \(M\) with \(W \cap U = 0\) and \(W + U = M\).

public theorem _root_.LieModule.exists_isCompl_of_isSemisimple
    {K L M : Type*} [Field K] [CharZero K] [LieRing L]
    [LieAlgebra K L] [Module.Finite K L] [LieAlgebra.IsSemisimple K L]
    [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M]
    [Module.Finite K M] (W : LieSubmodule K L M) :
    ∃ U : LieSubmodule K L M, IsCompl W U

Used by 1

Used byLevi decomposition

TheoremLevi decomposition#✓fully proved

Let \(L\) be a finite-dimensional Lie algebra over a field \(K\) of characteristic zero, and let \(\operatorname{rad}(L)\) be its radical, the largest solvable ideal of \(L\). Then there is a semisimple Lie subalgebra \(S\) of \(L\) (a Levi factor) such that \(L = \operatorname{rad}(L) \oplus S\) as \(K\)-vector spaces, that is, \(\operatorname{rad}(L) + S = L\) and \(\operatorname{rad}(L) \cap S = 0\).

Proof: Weyl's complete reducibility theorem is proved with the trace-form Casimir operator. The Levi factor is then constructed for an abelian radical and the general case follows by induction through the derived ideal of the radical.

public theorem levi_decomposition
    {K L : Type*} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L]
    [Module.Finite K L] :
    ∃ (S : LieSubalgebra K L), LieAlgebra.IsSemisimple K S ∧
      (↑(LieAlgebra.radical K L) + (S : Submodule K L) = (⊤ : Submodule K L)) ∧
      (↑(LieAlgebra.radical K L) ⊓ (S : Submodule K L) = (⊥ : Submodule K L))

Sources

• E. E. Levi, Atti Accad. Sci. Torino 1905 and A. I. Malcev, Izv. Akad. Nauk SSSR 1945; Bourbaki, Lie I; Lean states K-module direct sum form over char-zero fields.

Uses 1 · Used by 1

Proof usesWeyl's complete reducibility theorem

Used byAdo's theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.