Maximal-dimensional solvable-radical candidates

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. A solvable-radical candidate is a connected normal smooth solvable closed subgroup. Such candidates are closed under scheme-theoretic multiplication images, so the general maximal-dimension theorem for product-closed families applies: a candidate of maximal Lie dimension contains every other candidate.

Main declaration

• TauCeti.HopfIdeal.IsSolvableRadicalCandidate.le_of_finrank_maximal: a maximal-dimensional solvable-radical candidate is the greatest candidate.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 5.a, 6.a, 10.a.
• A. Borel, Linear Algebraic Groups, Section 11.21.

The specialization follows the formal pattern of TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.Maximal, using the shared theorem in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Normal.Product.Maximal.

This is the maximal-dimension comparison used to construct the solvable radical in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.le_of_finrank_maximal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) (hmax : ∀ (K : HopfIdeal k ↑H.obj), IsSolvableRadicalCandidate H K → Module.finrank k (Derivation k (↑H.obj ⧸ K.toIdeal) (Bialgebra.CounitAlgebra k (↑H.obj ⧸ K.toIdeal) k)) ≤ Module.finrank k (Derivation k (↑H.obj ⧸ I.toIdeal) (Bialgebra.CounitAlgebra k (↑H.obj ⧸ I.toIdeal) k))) (hJ : IsSolvableRadicalCandidate H J) : I ≤ J

A maximal-dimensional solvable-radical candidate is the greatest candidate.

The order on Hopf ideals reverses inclusion of represented closed subgroups: I ≤ J says that the subgroup cut out by I contains the subgroup cut out by J.