Unipotent radicals and reductive quotients

This file applies ground-field triviality of the radical of a reductive group to an exact-sequence criterion. Suppose a homomorphism of affine groups is represented contravariantly by an injective coordinate map f : D ⟶ H. If its kernel is connected, normal, smooth, and unipotent, and the quotient group represented by D is reductive, then the kernel is the unipotent radical of the group represented by H.

The reverse containment sends the unipotent radical through the quotient map. Its scheme-theoretic image remains connected, smooth, and unipotent; injectivity of f makes it normal in the quotient. Reductivity therefore makes that image trivial.

Main declarations

• The trivial-radical criterion identifies a connected normal smooth unipotent kernel with the radical when the target radical is trivial.
• TauCeti.FiniteTypeCommHopfAlgCat. unipotentRadicalDefiningIdeal_eq_kernelHopfIdeal_of_reductive: a connected normal smooth unipotent kernel with reductive quotient is the unipotent radical.

References

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

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_kernelHopfIdeal_of_unipotentRadicalDefiningIdeal_eq_augmentation {k : Type u} [Field k] (H D : FiniteTypeCommHopfAlgCat k) (hD : D.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑D.obj) (f : D.obj ⟶ H.obj) (hf_injective : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) (hf : HopfIdeal.IsUnipotentRadicalCandidate H (CommHopfAlgCat.kernelHopfIdeal f)) : H.unipotentRadicalDefiningIdeal = CommHopfAlgCat.kernelHopfIdeal f

A connected normal smooth unipotent kernel of a schematically dominant homomorphism to a group with trivial unipotent radical is the unipotent radical.

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_kernelHopfIdeal_of_reductive {k : Type u} [Field k] (H D : FiniteTypeCommHopfAlgCat k) (hD : reductiveCommHopfAlgProperty k D) (f : D.obj ⟶ H.obj) (hf_injective : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) (hf : HopfIdeal.IsUnipotentRadicalCandidate H (CommHopfAlgCat.kernelHopfIdeal f)) : H.unipotentRadicalDefiningIdeal = CommHopfAlgCat.kernelHopfIdeal f

A connected normal smooth unipotent kernel of a quotient homomorphism to a reductive group is the unipotent radical.