Lie algebras of solvable affine groups

A geometrically reduced, geometrically connected finite-type affine group with solvable geometric points has solvable Lie algebra, in every characteristic. Over an algebraically closed field, Lie--Kolchin embeds the group into an upper triangular general linear group. The differential is injective and the upper triangular tangent Lie algebra is solvable. Scalar extension and faithful-flat descent of Lie solvability give the general field case.

In characteristic zero this completes the equivalence between geometric solvability of a geometrically connected group and solvability of its Lie algebra. The reverse implication is geometricallySolvablePointsCommHopfAlgProperty.of_geometricallyConnected_of_isSolvable_lie. This comparison is used when relating solvable group radicals to Lie-algebra radicals.

Reducedness is essential in positive characteristic: geometric points alone do not detect infinitesimal groups. Connectedness is essential for the characteristic-zero converse, since a finite group has zero Lie algebra.

References

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

theorem TauCeti.isSolvable_lieAlgebra_of_isSolvable_points {k : Type u} [Field k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [IsReduced ↑H.obj] [ConnectedSpace (PrimeSpectrum ↑H.obj)] [Group.IsSolvable (WithConv (↑H.obj →ₐ[k] k))] : LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))

Over an algebraically closed field, a reduced connected affine group of finite type with solvable rational points has solvable Lie algebra, in every characteristic.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.isSolvable_lieAlgebra {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} [Algebra.IsGeometricallyReduced k ↑H.obj] (hsolv : geometricallySolvablePointsCommHopfAlgProperty k H.obj) (hconn : geometricallyConnectedCommHopfAlgProperty k H.obj) : LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))

The Lie algebra of a geometrically reduced and geometrically connected solvable affine group of finite type is solvable, over every field.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff_isSolvable_lieAlgebra {k : Type u} [Field k] [CharZero k] {H : FiniteTypeCommHopfAlgCat k} (hconn : geometricallyConnectedCommHopfAlgProperty k H.obj) : geometricallySolvablePointsCommHopfAlgProperty k H.obj ↔ LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))

A geometrically connected finite-type affine group in characteristic zero is geometrically solvable exactly when its Lie algebra is solvable. Smoothness follows from Cartier's theorem.