Candidates for the unipotent radical

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

This file proves the boundedness step in the standard maximal-dimension construction. The trivial subgroup, cut out by the augmentation ideal, is a candidate. The Lie dimension of every candidate is bounded by the Lie dimension of the ambient group, by the conormal exact sequence. Consequently the set of Lie dimensions attained by candidates is a nonempty finite set of natural numbers, and some candidate has maximal Lie dimension.

Binary-product closure is the next step: once the product of two candidates is again a candidate, a maximal-dimension candidate contains every other one and is the unipotent radical.

Main declarations

• TauCeti.HopfIdeal.IsUnipotentRadicalCandidate: a connected normal smooth unipotent closed subgroup in coordinate-Hopf-algebra form.
• TauCeti.HopfIdeal.isUnipotentRadicalCandidate_augmentation: the identity subgroup is a candidate.
• TauCeti.HopfIdeal.finrank_quotientLie_le: the Lie dimension of a closed subgroup is bounded by that of the ambient affine group.
• TauCeti.HopfIdeal.exists_isUnipotentRadicalCandidate_maximal_finrank_quotientLie: existence of a 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 5, "The unipotent radical", of the ReductiveGroups roadmap. It supplies the maximal-dimension choice used after closure of connected normal smooth unipotent subgroups under binary products.

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

A Hopf ideal cuts out an unipotent-radical candidate when the represented closed subgroup is normal, geometrically connected, smooth, and geometrically unipotent.

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.IsUnipotentRadicalCandidate.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_smoothUnipotent : smoothUnipotentCommHopfAlgProperty k (H.quotient I)) : IsUnipotentRadicalCandidate H I

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

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

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

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

A unipotent-radical candidate is geometrically connected.

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

A unipotent-radical candidate is smooth unipotent.

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

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

theorem TauCeti.HopfIdeal.exists_isUnipotentRadicalCandidate_maximal_finrank_quotientLie {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : ∃ (I : HopfIdeal k ↑H.obj), IsUnipotentRadicalCandidate H I ∧ ∀ (J : HopfIdeal k ↑H.obj), IsUnipotentRadicalCandidate 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 unipotent closed subgroup of maximal Lie dimension.

The theorem asserts maximality only among unipotent-radical candidates. Turning this candidate into the greatest such subgroup requires the separate binary-product theorem: the product with any other candidate is again a candidate and cannot have larger dimension.