Normal subgroups with solvable Lie algebra

Over an algebraically closed field of characteristic zero, the identity component of a normal closed subgroup with solvable Lie algebra lies in the solvable radical. Consequently the subgroup's entire tangent Lie algebra lies in the tangent Lie algebra of the radical. The subgroup itself can be disconnected, and need not lie in the radical.

For a connected ambient group, the Lie algebra of its solvable radical is exactly the radical of its Lie algebra. This comparison links group-theoretic semisimplicity with Lie-algebra semisimplicity and Cartan's criterion.

This is the passage from a normal subgroup realizing a solvable Lie ideal to containment of that ideal in Lie(R(G)). It uses the solvable-Lie-algebra criterion from Solvable.Lie, the invariance of the Lie algebra under passage to the identity component, and the universal property of the group radical. Smoothness follows from Cartier's theorem.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 10 and 22.
• J. E. Humphreys, Linear Algebraic Groups, §13.

theorem TauCeti.HopfIdeal.IsNormal.isSolvableRadicalCandidate_identityComponent {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : I.IsNormal) [LieAlgebra.IsSolvable ↥I.lieSubalgebra] : IsSolvableRadicalCandidate H I.identityComponent

The identity component of a normal closed subgroup with solvable Lie algebra is a connected normal smooth solvable closed subgroup in characteristic zero.

theorem TauCeti.HopfIdeal.IsNormal.lieSubalgebra_le_solvableRadical {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : I.IsNormal) [LieAlgebra.IsSolvable ↥I.lieSubalgebra] : I.lieSubalgebra ≤ H.solvableRadicalDefiningIdeal.lieSubalgebra

The tangent Lie algebra of a normal closed subgroup with solvable Lie algebra lies in the tangent Lie algebra of the solvable radical, even if that subgroup is disconnected.

theorem TauCeti.FiniteTypeCommHopfAlgCat.lieIdeal_solvableRadicalDefiningIdeal_eq_radical {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] (H : FiniteTypeCommHopfAlgCat k) [ConnectedSpace (PrimeSpectrum ↑H.obj)] : ⋯.lieIdeal = LieAlgebra.radical k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))

For a connected affine group over an algebraically closed field of characteristic zero, the Lie algebra of its solvable radical equals the solvable radical of its Lie algebra.