Reductive Lie algebras: the centre and the derived ideal span, and a converse criterion

A finite-dimensional Lie algebra L over a field of characteristic zero is reductive when its solvable radical is its centre, Mathlib's LieAlgebra.HasCentralRadical. This file proves that a reductive Lie algebra is spanned by its centre and its derived ideal,

center K L ⊔ ⁅L, L⁆ = ⊤ (TauCeti.sup_center_derivedSeries_eq_top),

and draws the consequences the representation theory of a reductive Lie algebra runs on: the derived ideal is perfect, equivariance of a linear map may be tested on the centre and on the derived ideal, and a finite-dimensional irreducible module over L stays irreducible over the derived ideal (TauCeti.isIrreducible_restrict_derivedSeries).

It also proves the converse criterion. If the derived ideal ⁅L, L⁆ has no nonzero solvable ideals (LieAlgebra.HasTrivialRadical, which a semisimple Lie algebra has) then L is reductive (TauCeti.hasCentralRadical_of_hasTrivialRadical_derivedSeries) and every solvable ideal, the centre among them, meets ⁅L, L⁆ only in ⊥ (TauCeti.inf_derivedSeries_eq_bot_of_isSolvable). That much is elementary and much cheaper than the spanning half: it holds over any commutative ring and needs no Killing form, no characteristic-zero hypothesis, no finite dimension and no Noetherian hypothesis.

Over a field of characteristic zero and in finite dimension, where the spanning half is available, the two combine into a direct sum

L = Z(L) ⊕ ⁅L, L⁆

(TauCeti.isCompl_center_derivedSeries_of_hasTrivialRadical_derivedSeries), which therefore carries those hypotheses even though the criterion itself does not.

The argument for the criterion

For a solvable ideal J the bracket ⁅L, J⁆ lies in J, because that is an ideal, and in ⁅L, L⁆, because every bracket does. The intersection J ⊓ ⁅L, L⁆ is a solvable ideal of L inside ⁅L, L⁆, hence — read as an ideal of the Lie algebra ⁅L, L⁆ through LieIdeal.restrict of TauCeti/Algebra/Lie/Solvable.lean — a solvable ideal of an algebra with trivial radical, so it vanishes. An element of J therefore brackets to zero against everything: it is central. The radical is the supremum of the solvable ideals, so it is central too — that is reductivity, and no finiteness hypothesis is needed because the radical itself never has to be solvable. The centre is one of those solvable ideals, so it meets ⁅L, L⁆ trivially, which is directness of the sum.

The argument for the spanning half

Everything comes from the Killing form κ and its orthogonal complements (LieIdeal.killingCompl). Cartan's criterion, in the form LieAlgebra.killingCompl_top_le_radical, says that the radical of κ is contained in the solvable radical; for a reductive L that radical is the centre, and the reverse inclusion is immediate because a central element has vanishing adjoint action. So the radical of κ is the centre (TauCeti.killingCompl_top_eq_center).

The derived ideal has the same orthogonal complement (TauCeti.killingCompl_derivedSeries_eq_center). Indeed the invariance κ ⁅x, y⁆ z = κ x ⁅y, z⁆ turns "x is orthogonal to every bracket" into "⁅y, x⁆ is orthogonal to everything", that is into ⁅y, x⁆ ∈ center K L for every y. The elements with that property are the normalizer of the centre, an ideal whose derived ideal is central and therefore abelian: it is a solvable ideal, so reductivity puts it back inside the centre. This is TauCeti.normalizer_center_eq_center.

Two subspaces of a finite-dimensional space with the same orthogonal complement for a symmetric form need not be equal — but they are if both contain the radical of the form, and the dimension formula LinearMap.BilinForm.finrank_add_finrank_orthogonal makes that precise. Applied to center K L ⊔ ⁅L, L⁆, whose orthogonal complement is the centre by the two computations above and which contains the centre for trivial reasons, it forces that ideal to be everything.

Main results

• TauCeti.normalizer_center_eq_center: over a reductive Lie algebra the centre is its own normalizer, because the normalizer is a solvable ideal (TauCeti.isSolvable_normalizer_center).
• TauCeti.killingCompl_top_eq_center and TauCeti.killingCompl_derivedSeries_eq_center: the radical of the Killing form and the orthogonal complement of the derived ideal are both the centre.
• TauCeti.sup_center_derivedSeries_eq_top: the centre and the derived ideal span, center K L ⊔ ⁅L, L⁆ = ⊤, with TauCeti.exists_mem_center_add_mem_derivedSeries its elementwise form.
• TauCeti.lie_derivedSeries_derivedSeries_eq_self: the derived ideal is perfect.
• TauCeti.map_lie_of_forall_center_of_forall_derivedSeries and TauCeti.lieModuleEquivOfCenterOfDerivedSeries: a linear map equivariant for the centre and for the derived ideal is equivariant for L, so a derived-ideal equivalence between modules on which the centre acts by the same scalars is an L-equivalence.
• TauCeti.isIrreducible_restrict_derivedSeries: a finite-dimensional irreducible module over a reductive Lie algebra restricts to an irreducible module over the derived ideal, over an algebraically closed field.
• TauCeti.inf_derivedSeries_eq_bot_of_isSolvable and TauCeti.le_center_of_isSolvable: when the derived ideal has trivial radical, every solvable ideal is central, meeting the derived ideal only in ⊥.
• TauCeti.hasCentralRadical_of_hasTrivialRadical_derivedSeries: a Lie algebra whose derived ideal has trivial radical is reductive, with TauCeti.radical_le_center_of_hasTrivialRadical_derivedSeries the inclusion it rests on.
• TauCeti.isCompl_center_derivedSeries_of_hasTrivialRadical_derivedSeries: such a Lie algebra is the direct sum of its centre and its derived ideal, over a field of characteristic zero and in finite dimension.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §6.4.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §5 and §6.

The centre is its own normalizer

theorem TauCeti.isSolvable_normalizer_center (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] : LieAlgebra.IsSolvable ↥(LieSubmodule.normalizer (LieAlgebra.center K L))

The elements x for which ⁅y, x⁆ is central for every y — that is, the normalizer of the centre — form a solvable ideal: its derived ideal is central, hence abelian.

theorem TauCeti.normalizer_center_eq_center (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] [IsNoetherian K L] [LieAlgebra.HasCentralRadical K L] : LieSubmodule.normalizer (LieAlgebra.center K L) = LieAlgebra.center K L

Over a reductive Lie algebra the centre is its own normalizer. The normalizer is a solvable ideal by TauCeti.isSolvable_normalizer_center, hence lies in the radical, which is the centre.

theorem TauCeti.mem_center_of_forall_lie_mem_center (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] [IsNoetherian K L] [LieAlgebra.HasCentralRadical K L] {x : L} (h : ∀ (y : L), ⁅y, x⁆ ∈ LieAlgebra.center K L) : x ∈ LieAlgebra.center K L

A convenient elementwise form of TauCeti.normalizer_center_eq_center: over a reductive Lie algebra, if every bracket ⁅y, x⁆ is central, then x itself is central.

The Killing form sees only the centre

theorem TauCeti.killingCompl_top_eq_center (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] : LieIdeal.killingCompl K L ⊤ = LieAlgebra.center K L

For a reductive Lie algebra the radical of the Killing form is the centre. One inclusion is Cartan's criterion LieAlgebra.killingCompl_top_le_radical together with reductivity; the other holds because a central element acts by zero.

theorem TauCeti.lie_mem_killingCompl_top_of_mem_killingCompl_derivedSeries {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] {x : L} (hx : x ∈ LieIdeal.killingCompl K L (LieAlgebra.derivedSeries K L 1)) (y : L) : ⁅y, x⁆ ∈ LieIdeal.killingCompl K L ⊤

An element orthogonal to the derived ideal brackets into the radical of the Killing form: this is the invariance κ ⁅x, y⁆ z = κ x ⁅y, z⁆ read from right to left.

theorem TauCeti.killingCompl_derivedSeries_eq_center (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] : LieIdeal.killingCompl K L (LieAlgebra.derivedSeries K L 1) = LieAlgebra.center K L

The derived ideal of a reductive Lie algebra has the centre as its orthogonal complement. Nothing beyond the radical of the Killing form is orthogonal to the derived ideal: an element orthogonal to it normalizes the centre by TauCeti.lie_mem_killingCompl_top_of_mem_killingCompl_derivedSeries, hence is central.

theorem TauCeti.killingCompl_sup_center_derivedSeries_eq_center (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] : LieIdeal.killingCompl K L (LieAlgebra.center K L ⊔ LieAlgebra.derivedSeries K L 1) = LieAlgebra.center K L

The orthogonal complement of the centre together with the derived ideal is again the centre: it is squeezed between the complements of the derived ideal and of the whole algebra, which TauCeti.killingCompl_derivedSeries_eq_center and TauCeti.killingCompl_top_eq_center identify with one another.

The centre and the derived ideal span

theorem TauCeti.sup_center_derivedSeries_eq_top (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] : LieAlgebra.center K L ⊔ LieAlgebra.derivedSeries K L 1 = ⊤

The centre and the derived ideal of a reductive Lie algebra span it: L = Z(L) + ⁅L, L⁆.

The ideal center K L ⊔ ⁅L, L⁆ and the whole algebra have the same orthogonal complement for the Killing form, namely the centre, and both contain the radical of that form. The dimension formula LinearMap.BilinForm.finrank_add_finrank_orthogonal then equates their dimensions.

theorem TauCeti.exists_mem_center_add_mem_derivedSeries (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] (x : L) : ∃ z ∈ LieAlgebra.center K L, ∃ d ∈ LieAlgebra.derivedSeries K L 1, z + d = x

Every element of a reductive Lie algebra is a central element plus an element of the derived ideal.

theorem TauCeti.lie_derivedSeries_derivedSeries_eq_self (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] : ⁅LieAlgebra.derivedSeries K L 1, LieAlgebra.derivedSeries K L 1⁆ = LieAlgebra.derivedSeries K L 1

The derived ideal of a reductive Lie algebra is perfect: ⁅⁅L, L⁆, ⁅L, L⁆⁆ = ⁅L, L⁆. A central element contributes nothing to a bracket, so writing both arguments of a generating bracket of ⁅L, L⁆ as a central element plus an element of ⁅L, L⁆ leaves only the brackets of the derived ideal with itself.

Triviality of the radical of the derived ideal is a criterion for reductivity

@[simp]

theorem TauCeti.inf_derivedSeries_eq_bot_of_isSolvable (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.derivedSeries K L 1)] (J : LieIdeal K L) [LieAlgebra.IsSolvable ↥J] : J ⊓ ⁅⊤, ⊤⁆ = ⊥

A solvable ideal meets the derived ideal trivially when the derived ideal has no nonzero solvable ideals. The intersection is a solvable ideal of L lying inside ⁅L, L⁆, so it is an ideal of ⁅L, L⁆ (LieIdeal.restrict) that LieAlgebra.HasTrivialRadical kills.

The derived ideal is spelled ⁅⊤, ⊤⁆ rather than derivedSeries K L 1 so that the left-hand side is in simp-normal form; the two are definitionally equal.

theorem TauCeti.le_center_of_isSolvable (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.derivedSeries K L 1)] (J : LieIdeal K L) [LieAlgebra.IsSolvable ↥J] : J ≤ LieAlgebra.center K L

Every solvable ideal is central when the derived ideal has no nonzero solvable ideals.

The bracket ⁅L, J⁆ lands in J, because that is an ideal, and in ⁅L, L⁆, because every bracket does; so it lands in their intersection, which is ⊥ by TauCeti.inf_derivedSeries_eq_bot_of_isSolvable. An element of J therefore has vanishing bracket with everything, which is membership in the centre.

theorem TauCeti.radical_le_center_of_hasTrivialRadical_derivedSeries (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.derivedSeries K L 1)] : LieAlgebra.radical K L ≤ LieAlgebra.center K L

The radical of a Lie algebra whose derived ideal has trivial radical is central.

The radical is the supremum of the solvable ideals, and TauCeti.le_center_of_isSolvable puts each of them inside the centre. Passing through the supremum this way avoids any finiteness hypothesis: the radical itself never has to be solvable.

theorem TauCeti.hasCentralRadical_of_hasTrivialRadical_derivedSeries (K : Type u) (L : Type v) [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.derivedSeries K L 1)] : LieAlgebra.HasCentralRadical K L

A Lie algebra whose derived ideal has trivial radical is reductive.

This is the converse direction of the structure theorem for reductive Lie algebras, and it needs no field of characteristic zero, no finite dimension and no Noetherian hypothesis. Nor does it need the centre and the derived ideal to be complementary: triviality of the radical of ⁅L, L⁆ alone forces radical K L = center K L. Complementarity is a further consequence, but only over a field of characteristic zero and in finite dimension, where the spanning half TauCeti.sup_center_derivedSeries_eq_top is available (TauCeti.isCompl_center_derivedSeries_of_hasTrivialRadical_derivedSeries).

theorem TauCeti.isCompl_center_derivedSeries_of_hasTrivialRadical_derivedSeries (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.derivedSeries K L 1)] : IsCompl (LieAlgebra.center K L) (LieAlgebra.derivedSeries K L 1)

A Lie algebra whose derived ideal has trivial radical is the direct sum of its centre and that ideal: L = Z(L) ⊕ ⁅L, L⁆, over a field of characteristic zero and in finite dimension.

Reductivity comes from TauCeti.hasCentralRadical_of_hasTrivialRadical_derivedSeries, which needs neither hypothesis; the sum comes from TauCeti.sup_center_derivedSeries_eq_top, which is where both of them are spent; and the directness comes from TauCeti.inf_derivedSeries_eq_bot_of_isSolvable applied to the centre, which is abelian and therefore a solvable ideal.

Modules over a reductive Lie algebra

theorem TauCeti.map_lie_of_forall_center_of_forall_derivedSeries (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule L N] (f : M →ₗ[K] N) (hZ : ∀ z ∈ LieAlgebra.center K L, ∀ (m : M), f ⁅z, m⁆ = ⁅z, f m⁆) (hD : ∀ d ∈ LieAlgebra.derivedSeries K L 1, ∀ (m : M), f ⁅d, m⁆ = ⁅d, f m⁆) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆

Equivariance is tested on the centre and on the derived ideal. A linear map between L-modules commuting with the action of every central element and of every element of ⁅L, L⁆ commutes with the action of L, because those two ideals span (TauCeti.sup_center_derivedSeries_eq_top).

def TauCeti.lieModuleEquivOfCenterOfDerivedSeries (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule L N] (e : M ≃ₗ[K] N) (hZ : ∀ z ∈ LieAlgebra.center K L, ∀ (m : M), e ⁅z, m⁆ = ⁅z, e m⁆) (hD : ∀ d ∈ LieAlgebra.derivedSeries K L 1, ∀ (m : M), e ⁅d, m⁆ = ⁅d, e m⁆) : M ≃ₗ⁅K,L⁆ N

A linear equivalence which is equivariant for the derived ideal and for the centre is an equivalence of L-modules. This is the dictionary through which the representation theory of the derived ideal — the semisimple part — reaches L: the centre contributes only the scalars recorded by TauCeti.centralWeight.

Equations

• TauCeti.lieModuleEquivOfCenterOfDerivedSeries K L e hZ hD = { toLinearMap := ↑e, map_lie' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.lieModuleEquivOfCenterOfDerivedSeries_apply (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule L N] (e : M ≃ₗ[K] N) (hZ : ∀ z ∈ LieAlgebra.center K L, ∀ (m : M), e ⁅z, m⁆ = ⁅z, e m⁆) (hD : ∀ d ∈ LieAlgebra.derivedSeries K L 1, ∀ (m : M), e ⁅d, m⁆ = ⁅d, e m⁆) (m : M) : (lieModuleEquivOfCenterOfDerivedSeries K L e hZ hD) m = e m

@[simp]

theorem TauCeti.lieModuleEquivOfCenterOfDerivedSeries_symm_apply (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] {N : Type w'} [AddCommGroup N] [Module K N] [LieRingModule L N] (e : M ≃ₗ[K] N) (hZ : ∀ z ∈ LieAlgebra.center K L, ∀ (m : M), e ⁅z, m⁆ = ⁅z, e m⁆) (hD : ∀ d ∈ LieAlgebra.derivedSeries K L 1, ∀ (m : M), e ⁅d, m⁆ = ⁅d, e m⁆) (n : N) : (lieModuleEquivOfCenterOfDerivedSeries K L e hZ hD).symm n = e.symm n

theorem TauCeti.isIrreducible_restrict_derivedSeries (K : Type u) (L : Type v) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.HasCentralRadical K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsAlgClosed K] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : LieModule.IsIrreducible K (↥(LieAlgebra.derivedSeries K L 1)) M

The semisimple part acts irreducibly. A finite-dimensional irreducible module over a reductive Lie algebra, over an algebraically closed field, restricts to an irreducible module over the derived ideal.

The centre acts by scalars (TauCeti.exists_centralWeight_of_isIrreducible), so every subspace of M is stable under it; since the centre and the derived ideal span, a submodule for the derived ideal is already a submodule for L. Algebraic closedness is essential and not a convenience: over ℝ the one-dimensional abelian Lie algebra acting on ℝ² by the rotation generator is irreducible, is its own centre, and has zero derived ideal.

Together with the central weight, this shows that every finite-dimensional irreducible determines an irreducible restricted module and a functional on the centre; reconstruction and uniqueness are not asserted here.