The Lie algebra of a solvable-radical candidate

The tangent Lie ideal of a smooth geometrically connected solvable normal closed subgroup lies in the solvable radical of the ambient Lie algebra. This applies in particular to the group's solvable radical, using FiniteTypeCommHopfAlgCat.isSolvableRadicalCandidate_solvableRadicalDefiningIdeal.

Normality makes the tangent image an ideal. Its solvability follows from geometricallySolvablePointsCommHopfAlgProperty.isSolvable_lieAlgebra, and the universal property of the Lie radical gives the containment. No characteristic assumption or smoothness of the ambient group is needed. If the ambient Lie radical vanishes, every such subgroup is trivial: its Lie algebra is zero and its coordinate algebra is connected. Equality with the Lie radical is not asserted.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 10 and 16.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.lieIdeal_le_radical {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) : ⋯.lieIdeal ≤ LieAlgebra.radical k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))

The tangent Lie ideal of a connected smooth solvable normal closed subgroup is contained in the radical of the ambient tangent Lie algebra, in every characteristic.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.eq_augmentation_of_hasTrivialRadical {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) [LieAlgebra.HasTrivialRadical k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] : I = augmentation k ↑H.obj

A connected smooth solvable normal closed subgroup is trivial if the ambient Lie algebra has trivial solvable radical. The ambient group need not be smooth or connected, and the field may have any characteristic.