Solvability along Lie homomorphisms, the radical of a quotient, and ideals inside an ideal

Mathlib transports solvability of a Lie algebra along injective and surjective homomorphisms and shows that a sum of two solvable ideals is solvable, but it does not record the third and most frequently used closure property: solvability is an extension property. A Lie algebra with a solvable ideal whose quotient is solvable is itself solvable. This file proves that, in the sharper form that an ideal is solvable as soon as its image under some homomorphism is solvable and the part of it inside the kernel is, and draws the consequence that the solvable radical is carried onto the solvable radical by a surjective homomorphism with solvable kernel.

A last section changes direction and looks inside an ideal rather than along a homomorphism. An ideal J of L contained in an ideal I is also an ideal of the Lie algebra ↥I, namely LieIdeal.restrict I J, the preimage of J under the inclusion I ↪ L; the two readings have the same elements, so J is trivial exactly when its reading inside I is, and it is solvable exactly when that reading is. Consequently a solvable ideal of L lying inside an ideal with trivial radical is trivial (LieIdeal.eq_bot_of_le_of_isSolvable), which is how a semisimplicity hypothesis on one ideal constrains the radical of the whole algebra.

The headline corollary is that the quotient of a Noetherian Lie algebra by its radical has trivial radical, so that the radical is the unique solvable ideal with that property. In characteristic zero, where LieAlgebra.HasTrivialRadical is Cartan's criterion for semisimplicity, this is the statement that L ⧸ radical R L is semisimple: the first step of the structure theory, and the missing input for identifying the radical of a scalar extension of L with the scalar extension of its radical.

Everything is phrased through LieAlgebra.derivedSeriesOfIdeal, the derived series of an ideal computed inside the ambient algebra, because the type ↥I makes images and preimages awkward. Mathlib already relates the two readings through LieIdeal.derivedSeries_eq_bot_iff, and the two new transport lemmas below are the exact analogues for a general starting ideal of Mathlib's LieIdeal.derivedSeries_map_le and LieIdeal.derivedSeries_map_eq, which treat the case of the whole algebra.

Main statements

• LieIdeal.derivedSeriesOfIdeal_map_le and LieIdeal.derivedSeriesOfIdeal_map_eq: the derived series of an ideal maps into, and for a surjective homomorphism onto, the derived series of the image.
• LieIdeal.isSolvable_map: the image of a solvable ideal under a surjective homomorphism is solvable.
• LieIdeal.isSolvable_of_isSolvable_map: solvability descends from the image together with the part of the ideal lying in the kernel.
• LieAlgebra.derivedAbelianOfIdeal_le: Mathlib's abelian ideal LieAlgebra.derivedAbelianOfIdeal of an ideal (the last nonzero term of its derived series when the ideal is solvable, and ⊥ otherwise) lies inside the ideal.
• LieAlgebra.isSolvable_of_isSolvable_ker_of_surjective and LieAlgebra.isSolvable_iff_ideal_quotient: solvability is an extension property.
• LieIdeal.radical_map_eq: a surjective homomorphism with solvable kernel carries the radical onto the radical.
• LieIdeal.restrict: an ideal of L read as an ideal of an ideal I of L, with LieIdeal.restrict_eq_bot_iff and LieIdeal.isSolvable_restrict_iff saying that for J ≤ I the two readings are trivial, respectively solvable, together, and LieIdeal.eq_bot_of_le_of_isSolvable: a solvable ideal inside an ideal with trivial radical is trivial.
• LieAlgebra.hasTrivialRadical_of_equiv: triviality of the radical transfers along an isomorphism of Lie algebras.
• LieAlgebra.hasTrivialRadical_quotient_radical: the quotient of a Noetherian Lie algebra by its radical has trivial radical, with LieAlgebra.radical_le_of_hasTrivialRadical_quotient and LieAlgebra.hasTrivialRadical_quotient_iff: the radical is the smallest ideal, and the only solvable one, whose quotient has trivial radical.

References

• [N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1-3][bourbaki1975], Chapter I, §5.
• N. Jacobson, Lie Algebras, Interscience (1962), Chapter III.

theorem LieIdeal.derivedSeriesOfIdeal_map_le {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (k : ℕ) : map f (LieAlgebra.derivedSeriesOfIdeal R L k I) ≤ LieAlgebra.derivedSeriesOfIdeal R L' k (map f I)

The image of the k-th term of the derived series of an ideal is contained in the k-th term of the derived series of the image.

This is LieIdeal.derivedSeries_map_le with ⊤ replaced by an arbitrary ideal.

theorem LieIdeal.derivedSeriesOfIdeal_map_eq {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (h : Function.Surjective ⇑f) (k : ℕ) : map f (LieAlgebra.derivedSeriesOfIdeal R L k I) = LieAlgebra.derivedSeriesOfIdeal R L' k (map f I)

A surjective Lie homomorphism carries the derived series of an ideal onto the derived series of the image.

This is LieIdeal.derivedSeries_map_eq with ⊤ replaced by an arbitrary ideal.

theorem LieIdeal.isSolvable_map {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (h : Function.Surjective ⇑f) [LieAlgebra.IsSolvable ↥I] : LieAlgebra.IsSolvable ↥(map f I)

The image of a solvable ideal under a surjective Lie homomorphism is solvable.

theorem LieIdeal.isSolvable_of_isSolvable_map {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (h₁ : LieAlgebra.IsSolvable ↥(I ⊓ f.ker)) (h₂ : LieAlgebra.IsSolvable ↥(map f I)) : LieAlgebra.IsSolvable ↥I

Solvability descends along a Lie homomorphism. An ideal is solvable as soon as its image is solvable and the part of it lying in the kernel is.

Taking f to be the quotient map by a solvable ideal and I to be ⊤ recovers the statement that an extension of a solvable Lie algebra by a solvable ideal is solvable, which is LieAlgebra.isSolvable_of_isSolvable_ker_of_surjective below.

theorem LieIdeal.radical_map_eq {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') [IsNoetherian R L] (h : Function.Surjective ⇑f) (hker : LieAlgebra.IsSolvable ↥f.ker) : map f (LieAlgebra.radical R L) = LieAlgebra.radical R L'

A surjective Lie homomorphism with solvable kernel carries the solvable radical onto the solvable radical.

Ideals inside an ideal

def LieIdeal.restrict {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) : LieIdeal R ↥I

An ideal of L, read inside an ideal I of L: the preimage of J under the inclusion I ↪ L. For J ≤ I this presents J itself as an ideal of the Lie algebra ↥I, which is what lets the ideal theory of ↥I speak about ideals of L that happen to lie in I.

Equations

• I.restrict J = LieIdeal.comap I.incl J

@[simp]

theorem LieIdeal.mem_restrict {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} {x : ↥I} : x ∈ I.restrict J ↔ ↑x ∈ J

instance LieIdeal.isSolvable_restrict {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) [LieAlgebra.IsSolvable ↥J] : LieAlgebra.IsSolvable ↥(I.restrict J)

Read inside an ideal, a solvable ideal stays solvable.

theorem LieIdeal.isSolvable_restrict_iff {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : J ≤ I) : LieAlgebra.IsSolvable ↥(I.restrict J) ↔ LieAlgebra.IsSolvable ↥J

An ideal contained in I is solvable exactly when it is solvable read inside I.

theorem LieIdeal.restrict_eq_bot_iff {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : J ≤ I) : I.restrict J = ⊥ ↔ J = ⊥

An ideal contained in I is trivial exactly when it is trivial read inside I.

theorem LieIdeal.eq_bot_of_le_of_isSolvable {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} [LieAlgebra.HasTrivialRadical R ↥I] (h : J ≤ I) [LieAlgebra.IsSolvable ↥J] : J = ⊥

A solvable ideal contained in an ideal with trivial radical is trivial. The ideals of L lying inside I are ideals of ↥I, and LieAlgebra.HasTrivialRadical kills the solvable ones.

theorem LieAlgebra.derivedAbelianOfIdeal_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : derivedAbelianOfIdeal I ≤ I

The ideal derivedAbelianOfIdeal I is contained in I. When I is solvable this is the last nonzero term of its derived series; otherwise it is ⊥.

theorem LieAlgebra.isSolvable_of_isSolvable_ker_of_surjective {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} (h : Function.Surjective ⇑f) (h₁ : IsSolvable ↥f.ker) (h₂ : IsSolvable L') : IsSolvable L

An extension of a solvable Lie algebra by a solvable ideal is solvable.

theorem LieAlgebra.isSolvable_iff_ideal_quotient {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsSolvable L ↔ IsSolvable ↥I ∧ IsSolvable (L ⧸ I)

Solvability is an extension property: a Lie algebra is solvable exactly when both an ideal and the quotient by it are.

theorem LieAlgebra.hasTrivialRadical_of_equiv {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [HasTrivialRadical R L] (e : L ≃ₗ⁅R⁆ L') : HasTrivialRadical R L'

Triviality of the radical transfers along an isomorphism of Lie algebras.

No finiteness hypothesis is needed: neither Lie algebra has to be Noetherian or finite-dimensional.

instance LieAlgebra.hasTrivialRadical_quotient_radical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : HasTrivialRadical R (L ⧸ radical R L)

The quotient of a Noetherian Lie algebra by its solvable radical has trivial radical.

Over a field of characteristic zero, where LieAlgebra.HasTrivialRadical is equivalent to semisimplicity by Cartan's criterion, this says that L ⧸ radical R L is semisimple.

theorem LieAlgebra.radical_le_of_hasTrivialRadical_quotient {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) [HasTrivialRadical R (L ⧸ I)] : radical R L ≤ I

The radical is the smallest ideal whose quotient has trivial radical. Its image in such a quotient is a solvable ideal, hence trivial.

@[simp]

theorem LieAlgebra.hasTrivialRadical_quotient_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) [IsSolvable ↥I] : HasTrivialRadical R (L ⧸ I) ↔ I = radical R L

The radical is the unique solvable ideal whose quotient has trivial radical.