Candidates for the solvable radical

Let H be the coordinate Hopf algebra of a finite-type affine group over a field. A candidate for its solvable radical is a connected normal smooth solvable closed subgroup. In Hopf coordinates this is a normal Hopf ideal I whose quotient H/I is geometrically connected, smooth, and has a solvable group of geometric points.

This file proves the boundedness step in the maximal-dimension construction. Every unipotent-radical candidate is a solvable-radical candidate, so in particular the identity subgroup is a candidate. The Lie dimension of every candidate is bounded by that of the ambient group. Hence the natural numbers occurring as candidate dimensions form a nonempty finite set, and one of the candidates has maximal Lie dimension.

To turn a maximal-dimensional candidate into the solvable radical, one must next show that the scheme-theoretic multiplication image of two candidates is again a candidate. The connectedness, smoothness, and source-solvability results already exist; the remaining input is solvability of the image, for which the current image theorem requires faithful flatness of the canonical Hopf image inclusion.

Main declarations

• TauCeti.HopfIdeal.IsSolvableRadicalCandidate: a connected normal smooth solvable closed subgroup in coordinate-Hopf-algebra form.
• TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.isSolvableRadicalCandidate: every unipotent-radical candidate is a solvable-radical candidate.
• TauCeti.HopfIdeal.isSolvableRadicalCandidate_augmentation: the identity subgroup is a candidate.
• TauCeti.HopfIdeal.exists_isSolvableRadicalCandidate_maximal_finrank_quotientLie: existence of a solvable-radical candidate of maximal Lie dimension.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and §§6.45–6.46.
• A. Borel, Linear Algebraic Groups, §11.21.

This advances Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. The radical R(G) required there is the greatest connected normal smooth solvable closed subgroup; the maximal-dimension candidate constructed here is the first step in that construction.

def TauCeti.HopfIdeal.IsSolvableRadicalCandidate {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) : Prop

A Hopf ideal cuts out a solvable-radical candidate when the represented closed subgroup is normal, geometrically connected, smooth, and has a solvable group of geometric points.

Normality is a property of the ideal in the ambient coordinate Hopf algebra. The other three conditions are properties of its finite-type quotient coordinate Hopf algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.mk {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (h_normal : I.IsNormal) (h_connected : geometricallyConnectedCommHopfAlgProperty k (H.quotient I).obj) (h_smooth : Algebra.Smooth k ↑(H.quotient I).obj) (h_solvable : geometricallySolvablePointsCommHopfAlgProperty k (H.quotient I).obj) : IsSolvableRadicalCandidate H I

A normal Hopf ideal with geometrically connected, smooth, solvable quotient is a solvable-radical candidate.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.isNormal {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) : I.IsNormal

A solvable-radical candidate is normal in the ambient affine group.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.geometricallyConnected {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) : geometricallyConnectedCommHopfAlgProperty k (H.quotient I).obj

A solvable-radical candidate is geometrically connected.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.smooth {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) : Algebra.Smooth k ↑(H.quotient I).obj

A solvable-radical candidate is smooth.

theorem TauCeti.HopfIdeal.IsSolvableRadicalCandidate.geometricallySolvable {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsSolvableRadicalCandidate H I) : geometricallySolvablePointsCommHopfAlgProperty k (H.quotient I).obj

A solvable-radical candidate has a solvable group of geometric points.

theorem TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.isSolvableRadicalCandidate {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑H.obj} (hI : IsUnipotentRadicalCandidate H I) : IsSolvableRadicalCandidate H I

Every unipotent-radical candidate is a solvable-radical candidate.

theorem TauCeti.HopfIdeal.isSolvableRadicalCandidate_augmentation {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : IsSolvableRadicalCandidate H (augmentation k ↑H.obj)

The augmentation ideal cuts out the identity subgroup, hence is a solvable-radical candidate. This makes the family of candidates nonempty without any hypothesis on the ambient finite-type affine group.

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

There exists a connected normal smooth solvable closed subgroup of maximal Lie dimension.

The theorem asserts maximality only among solvable-radical candidates. Turning this candidate into the greatest such subgroup requires closure of candidates under scheme-theoretic binary products.