Solvable groups from solvable Lie algebras

Over an algebraically closed field of characteristic zero, a connected affine group of finite type with solvable Lie algebra is solvable. More precisely, every finite-dimensional representation admits an upper-triangular basis, and the group embeds as a closed subgroup of an upper-triangular general linear group.

Lie's theorem gives a common eigenline for the differentiated representation. For connected groups in characteristic zero, Lie-stable subspaces are subcomodules, so this eigenline is a group weight line. Applying the same argument to successive quotients gives a full flag. A finite-dimensional coefficient-generating representation then supplies the closed embedding. In particular the points over every commutative value algebra form a solvable group, including value algebras with nilpotents. Over an arbitrary characteristic-zero field, a geometrically connected group with solvable Lie algebra is geometrically solvable, by scalar extension.

This criterion allows solvability of a connected closed subgroup to be established from its Lie algebra, as needed when comparing group radicals with Lie-algebra radicals. Connectedness is essential: finite groups in characteristic zero have zero Lie algebra.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 10, solvability and Lie algebras.
• J. E. Humphreys, Linear Algebraic Groups, §13.
• The eigenline argument uses Mathlib's LieModule.exists_nontrivial_weightSpace_of_isSolvable; integration of the eigenline uses Submodule.exists_subcomodule_iff_forall_differential_mem.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_isSolvable_lie {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] {M : Type w} [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] [Nontrivial M] : HasNonzeroWeightVector k (↑H.obj) M

A nonzero finite-dimensional representation of a connected group with solvable Lie algebra has a nonzero weight vector, over an algebraically closed field of characteristic zero.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperTriangular_of_isSolvable_lie {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] {M : Type w} [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperTriangular ∧ ∀ (i : Fin n), IsGroupLikeElem k (coefficientMatrix b i i)

Every finite-dimensional representation of a connected group with solvable Lie algebra is upper triangularizable in characteristic zero over an algebraically closed field.

theorem TauCeti.exists_upperTriangular_surjective_of_isSolvable_lie {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] : ∃ (n : ℕ) (f : GeneralLinear.UpperTriangular.coordinateHopfAlgebra k n ⟶ H.obj), Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

A connected affine group with solvable Lie algebra is a closed subgroup of an upper-triangular general linear group, in characteristic zero over an algebraically closed field. The surjection is in the contravariant coordinate direction.

theorem TauCeti.isSolvable_points_of_isSolvable_lie {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] (A : Type w) [CommRing A] [Algebra k A] : Group.IsSolvable (WithConv (↑H.obj →ₐ[k] A))

Every commutative-algebra-valued point group of a connected affine group with solvable Lie algebra is solvable, in characteristic zero over an algebraically closed field.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.of_isSolvable_lie {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsSolvable (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] : geometricallySolvablePointsCommHopfAlgProperty k H.obj

A connected affine group with solvable Lie algebra is geometrically solvable, in characteristic zero over an algebraically closed field.

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

Over any field of characteristic zero, a geometrically connected affine group of finite type with solvable Lie algebra is geometrically solvable.