The nilradical of a Lie algebra

The nilradical of a Lie algebra L is the supremum of its ideals that are nilpotent as Lie algebras, built here as Ado.LieAlgebra.nilradical R L, the supremum of the ideals I with LieRing.IsNilpotent I. As soon as L is Noetherian that supremum is itself nilpotent, so it is then a largest element: the largest nilpotent ideal. It sits between the centre and the solvable radical, and, again for Noetherian L, every one of its elements is ad-nilpotent.

Mathlib's LieAlgebra.maxNilpotentIdeal R L is a different ideal: the largest ideal on which the ambient algebra L acts nilpotently. It is contained in the nilradical (Ado.LieAlgebra.maxNilpotentIdeal_le_nilradical), and the containment is strict in general. The standard example is the two-dimensional nonabelian Lie algebra spanned by x and y with ⁅x, y⁆ = y: the span of y is an abelian, hence nilpotent, ideal, so it lies in the nilradical, while ⁅L, span y⁆ = span y says that L does not act nilpotently on it, and indeed no nonzero ideal of that algebra is acted on nilpotently, so its maxNilpotentIdeal is ⊥. That algebra is built in Ado.Algebra.Lie.AffineLine, where both ideals are computed and the containment is witnessed to be strict by Ado.LieAlgebra.AffineLine.maxNilpotentIdeal_lt_nilradical.

Nilpotency of an ideal, read inside the ambient algebra

Nilpotency of an ideal I as a Lie algebra is awkward to manipulate through the type ↥I, so the work below is done with Mathlib's LieIdeal.lcs I L, the descending series L ≥ ⁅I, L⁆ ≥ ⁅I, ⁅I, L⁆⁆ ≥ ⋯ of ideals of L. The two readings agree: LieIdeal.isNilpotent_iff_exists_lcs_eq_bot says that I is nilpotent as a Lie algebra exactly when that series reaches ⊥, equivalently (LieIdeal.isNilpotent_iff_isNilpotent_ambient) exactly when I acts nilpotently on the whole of L. From that description the sum of two nilpotent ideals is nilpotent, which is what makes the supremum defining the nilradical well behaved.

These ambient readings all take a LieIdeal as their receiver, so they live in the root LieIdeal namespace, where dot notation on that Mathlib type elaborates.

Main definitions

• Ado.LieAlgebra.nilradical: the supremum of the ideals of L that are nilpotent as Lie algebras, the largest such ideal as soon as L is Noetherian.

Main statements

• LieIdeal.isNilpotent_iff_exists_lcs_eq_bot and LieIdeal.isNilpotent_iff_isNilpotent_ambient: the two ambient readings of nilpotency of an ideal.
• LieIdeal.isNilpotentSup: a sum of nilpotent ideals is nilpotent.
• LieIdeal.exists_mem_notMem_lie_mem_of_lt: a proper subspace T of a nilpotent ideal I is enlarged by some x ∈ I with ⁅x, I⁆ ⊆ T.
• LieIdeal.le_nilradical and Ado.LieAlgebra.nilradical_le_iff: the two halves of the universal property of the supremum, neither needing a Noetherian assumption.
• Ado.LieAlgebra.nilradicalIsNilpotent: over a Noetherian Lie algebra the nilradical is nilpotent, so LieIdeal.isNilpotent_iff_le_nilradical characterises it.
• Ado.LieAlgebra.maxNilpotentIdeal_le_nilradical, Ado.LieAlgebra.center_le_nilradical and Ado.LieAlgebra.nilradical_le_radical: the standard containments.
• Ado.LieAlgebra.isNilpotent_ad_of_mem_nilradical: elements of the nilradical are ad-nilpotent.

References

• [N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1-3][bourbaki1975], Chapter I, §4.
• N. Jacobson, Lie Algebras, Interscience (1962), Chapter II.
• The construction of nilradical, nilradicalIsNilpotent, and the largest-ideal API adapts Mathlib's LieAlgebra.radical development in Mathlib.Algebra.Lie.Solvable.

theorem LieIdeal.lcs_antitone {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] (I : LieIdeal R L) : Antitone (I.lcs M)

The series M ≥ ⁅I, M⁆ ≥ ⁅I, ⁅I, M⁆⁆ ≥ ⋯ attached to an ideal is antitone.

theorem LieIdeal.lcs_mono {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] {I J : LieIdeal R L} (h : I ≤ J) (k : ℕ) : I.lcs M k ≤ J.lcs M k

The series M ≥ ⁅I, M⁆ ≥ ⁅I, ⁅I, M⁆⁆ ≥ ⋯ attached to an ideal is monotone in that ideal.

theorem LieIdeal.lcs_succ_le_map_lcs {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : I.lcs L (k + 1) ≤ LieSubmodule.map (LieSubmodule.incl I) (I.lcs (↥I) k)

The k + 1-st term of ⁅I, ⁅I, … ⁅I, L⁆…⁆⁆ lies in the image of the k-th term of the lower central series of I as a module over itself. This is the step that reads nilpotency of the Lie algebra ↥I back inside the ambient algebra.

theorem LieIdeal.lcs_eq_bot_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ℕ) : I.lcs M k = ⊥ ↔ LieModule.lowerCentralSeries R (↥I) M k = ⊥

The series ⁅I, ⁅I, … ⁅I, M⁆…⁆⁆ of submodules of M, read inside the ambient algebra, reaches ⊥ exactly when the lower central series of M as a module over I does.

theorem LieIdeal.isNilpotent_iff_exists_lcs_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieRing.IsNilpotent ↥I ↔ ∃ (k : ℕ), I.lcs L k = ⊥

An ideal is nilpotent as a Lie algebra exactly when the series ⁅I, ⁅I, … ⁅I, L⁆…⁆⁆ of ideals of the ambient algebra reaches ⊥.

theorem LieIdeal.isNilpotent_iff_isNilpotent_ambient {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieRing.IsNilpotent ↥I ↔ LieModule.IsNilpotent (↥I) L

An ideal is nilpotent as a Lie algebra exactly when it acts nilpotently on the whole of the ambient algebra.

theorem LieIdeal.isNilpotent_of_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : I ≤ J) : LieRing.IsNilpotent ↥J → LieRing.IsNilpotent ↥I

An ideal contained in a nilpotent ideal is itself nilpotent as a Lie algebra. This is the nilpotent counterpart of Mathlib's LieAlgebra.le_solvable_ideal_solvable.

theorem LieIdeal.isNilpotent_comap_of_injective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_3} [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L') (f : L →ₗ⁅R⁆ L') (hf : Function.Injective ⇑f) [LieRing.IsNilpotent ↥I] : LieRing.IsNilpotent ↥(comap f I)

The preimage of a nilpotent ideal under an injective Lie homomorphism is nilpotent.

theorem LieIdeal.isNilpotent_map_of_surjective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_3} [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (g : L →ₗ⁅R⁆ L') (hg : Function.Surjective ⇑g) (hI : LieRing.IsNilpotent ↥I) : LieRing.IsNilpotent ↥(map g I)

A surjective Lie algebra homomorphism maps a nilpotent ideal to a nilpotent ideal.

theorem LieIdeal.isNilpotent_map_equiv {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_3} [LieRing L'] [LieAlgebra R L'] (I : LieIdeal R L) (e : L ≃ₗ⁅R⁆ L') (hI : LieRing.IsNilpotent ↥I) : LieRing.IsNilpotent ↥(map e.toLieHom I)

A Lie algebra equivalence maps a nilpotent ideal to a nilpotent ideal.

theorem LieIdeal.isNilpotent_ad_of_mem {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRing.IsNilpotent ↥I] {x : L} (hx : x ∈ I) : IsNilpotent ((LieAlgebra.ad R L) x)

Every element of a nilpotent ideal acts nilpotently in the adjoint representation.

instance LieIdeal.isNilpotentBot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieRing.IsNilpotent ↥⊥

theorem LieIdeal.lcs_sup_le_iSup_inf {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (n : ℕ) : (I ⊔ J).lcs L n ≤ ⨆ (i : ℕ), I.lcs L i ⊓ J.lcs L (n - i)

The series of a supremum of two ideals is caught between the series of the two summands: after n steps every summand of the bound has spent i steps inside I and n - i steps inside J. This is the combinatorial heart of LieIdeal.isNilpotentSup.

instance LieIdeal.isNilpotentSup {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) [LieRing.IsNilpotent ↥I] [LieRing.IsNilpotent ↥J] : LieRing.IsNilpotent ↥(I ⊔ J)

A supremum of two nilpotent ideals is nilpotent.

theorem LieIdeal.exists_mem_notMem_lie_mem_of_lt {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRing.IsNilpotent ↥I] {T : Submodule R L} (hT : T < ↑I) : ∃ x ∈ I, x ∉ T ∧ ∀ y ∈ I, ⁅x, y⁆ ∈ T

A proper subspace of a nilpotent ideal is normalized by a new element of the ideal. If a submodule T lies strictly below a nilpotent ideal I, some x ∈ I outside T satisfies ⁅x, I⁆ ⊆ T. The element is taken from the last term of ⁅I, ⁅I, … ⁅I, L⁆…⁆⁆ not contained in T. When R is a field, I is finite-dimensional and T is a subalgebra, repeated application builds a flag of subalgebras from T up to I, each an ideal of the next with codimension one.

def Ado.LieAlgebra.nilradical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal R L

The nilradical of a Lie algebra: the supremum of the ideals that are nilpotent as Lie algebras. Over a Noetherian Lie algebra it is itself nilpotent, hence the largest nilpotent ideal.

This is not Mathlib's LieAlgebra.maxNilpotentIdeal, which is the largest ideal on which the ambient algebra acts nilpotently, and is in general smaller.

Equations

• Ado.LieAlgebra.nilradical R L = sSup {I : LieIdeal R L | LieRing.IsNilpotent ↥I}

instance Ado.LieAlgebra.nilradicalIsNilpotent (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieRing.IsNilpotent ↥(nilradical R L)

The nilradical of a Noetherian Lie algebra is nilpotent.

theorem LieIdeal.le_nilradical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (h : LieRing.IsNilpotent ↥I) : I ≤ Ado.LieAlgebra.nilradical R L

An ideal that is nilpotent as a Lie algebra is contained in the nilradical. This is the → direction of LieIdeal.isNilpotent_iff_le_nilradical, which needs no Noetherian assumption.

theorem Ado.LieAlgebra.nilradical_le_iff (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {J : LieIdeal R L} : nilradical R L ≤ J ↔ ∀ (I : LieIdeal R L), LieRing.IsNilpotent ↥I → I ≤ J

The nilradical is below an ideal J exactly when every nilpotent ideal is. This is the elimination half of the universal property of the supremum defining the nilradical, dual to LieIdeal.le_nilradical, and like it needs no Noetherian assumption.

theorem LieIdeal.isNilpotent_iff_le_nilradical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) : LieRing.IsNilpotent ↥I ↔ I ≤ Ado.LieAlgebra.nilradical R L

Over a Noetherian Lie algebra the nilradical is exactly the ideals nilpotent as Lie algebras.

The → direction holds without the Noetherian assumption; it is LieIdeal.le_nilradical.

theorem Ado.LieAlgebra.center_le_nilradical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.center R L ≤ nilradical R L

The centre is contained in the nilradical.

theorem Ado.LieAlgebra.nilradical_map_equiv (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_3} [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') : LieIdeal.map e.toLieHom (nilradical R L) = nilradical R L'

A Lie algebra equivalence carries the nilradical onto the nilradical. In particular, every Lie algebra automorphism preserves the nilradical.

theorem Ado.LieAlgebra.maxNilpotentIdeal_le_nilradical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.maxNilpotentIdeal R L ≤ nilradical R L

Mathlib's LieAlgebra.maxNilpotentIdeal is contained in the nilradical: an ideal on which the ambient algebra acts nilpotently is in particular nilpotent as a Lie algebra. The containment is strict in general: see Ado.LieAlgebra.AffineLine.maxNilpotentIdeal_lt_nilradical.

theorem Ado.LieAlgebra.nilradical_le_radical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : nilradical R L ≤ LieAlgebra.radical R L

The nilradical is contained in the solvable radical.

@[simp]

theorem Ado.LieAlgebra.nilradical_eq_top_of_isNilpotent (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] : nilradical R L = ⊤

The nilradical of a nilpotent Lie algebra is the whole Lie algebra.

@[simp]

theorem Ado.LieAlgebra.nilradical_eq_top_iff (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : nilradical R L = ⊤ ↔ LieRing.IsNilpotent L

Over a Noetherian Lie algebra, the nilradical is the whole algebra exactly when the algebra is nilpotent.

theorem Ado.LieAlgebra.isNilpotent_ad_of_mem_nilradical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] {x : L} (hx : x ∈ nilradical R L) : IsNilpotent ((LieAlgebra.ad R L) x)

Every element of the nilradical is ad-nilpotent.