Maximal-dimensional unipotent-radical candidates

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. The existing maximal-dimension construction chooses a connected normal smooth unipotent closed subgroup U whose Lie dimension is at least that of every other such subgroup. The existing product theorem shows that the scheme-theoretic product UV is another candidate containing both U and V.

The general maximal-dimension theorem for product-closed families now applies: smoothness and connectedness upgrade equality of tangent-space dimensions to UV = U. Consequently U contains every candidate.

Main declaration

• TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.le_of_finrank_maximal: a maximal-dimensional unipotent-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.

This completes the maximal-dimension step in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. The shared argument also supplies the corresponding comparison step for the solvable radical in Layer 6.

theorem TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.le_of_finrank_maximal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (hI : IsUnipotentRadicalCandidate H I) (hmax : ∀ (K : HopfIdeal k ↑H.obj), IsUnipotentRadicalCandidate 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 : IsUnipotentRadicalCandidate H J) : I ≤ J

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

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