Maximal-dimensional families of closed subgroups

Let H be the coordinate Hopf algebra of a finite-type affine group over a field, and let P be a family of smooth connected closed subgroups. Suppose a normal member I of P has maximal Lie dimension and the scheme-theoretic product of I with each member of P remains in P. Then I contains every other member.

Indeed, multiplying a maximal-dimensional member I by another member J gives a member that contains I. Dimension maximality then makes the resulting closed immersion an equality, by the comparison of TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Smooth.Dimension. Since the product also contains J, the subgroup represented by I contains J.

This argument is independent of the additional property defining the family. It is used for the unipotent radical and is also the dimension-comparison step in the construction of the solvable radical.

Main declaration

• TauCeti.HopfIdeal.le_of_product_of_finrank_maximal: a normal maximal-dimensional member of a family of smooth connected closed subgroups, closed under its products, is greatest.

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 supplies the shared maximal-dimension comparison used in Layers 5 and 6 of the ReductiveGroups roadmap to construct the unipotent and solvable radicals.

theorem TauCeti.HopfIdeal.le_of_product_of_finrank_maximal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I J : HopfIdeal k ↑H.obj} (P : HopfIdeal k ↑H.obj → Prop) (hI_normal : I.IsNormal) (connected : ∀ {K : HopfIdeal k ↑H.obj}, P K → ConnectedSpace (PrimeSpectrum (↑H.obj ⧸ K.toIdeal))) (smooth : ∀ {K : HopfIdeal k ↑H.obj}, P K → Algebra.Smooth k ↑(H.quotient K).obj) (product : ∀ {L : HopfIdeal k ↑H.obj}, P L → P (ker (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.productMapOfNormal H.obj I L hI_normal)))) (hI : P I) (hmax : ∀ (K : HopfIdeal k ↑H.obj), P 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 : P J) : I ≤ J

A normal maximal-dimensional member of a family of smooth connected closed subgroups contains every member when its product with each family member remains in the family.

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