The unipotent radical and reductivity

This file connects the construction of the geometric unipotent radical to the definition of a reductive finite-type affine group. It records that reductivity is equivalent to smoothness, geometric connectedness, and triviality of the unipotent radical after base change to an algebraic closure. It also records that the unipotent radical of a reductive group over its ground field is trivial.

Main declarations

• reductiveCommHopfAlgProperty_iff_unipotentRadicalDefiningIdeal_baseChange_eq_augmentation: reductivity is equivalent to smoothness, geometric connectedness, and triviality of the geometric unipotent radical.
• TauCeti.reductiveCommHopfAlgProperty.unipotentRadicalDefiningIdeal_eq_augmentation: a reductive group's unipotent radical over the ground field is trivial.

References

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

This connects Layer 5, "The unipotent radical", to the definition of reductivity in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.reductiveCommHopfAlgProperty_iff_unipotentRadicalDefiningIdeal_baseChange_eq_augmentation (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : reductiveCommHopfAlgProperty k H ↔ Algebra.Smooth k ↑H.obj ∧ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ H.baseChange.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

A finite-type affine group is reductive exactly when it is smooth and geometrically connected and its geometric unipotent radical is trivial.

theorem TauCeti.reductiveCommHopfAlgProperty.unipotentRadicalDefiningIdeal_eq_augmentation {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) : H.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj

The unipotent radical of a reductive finite-type affine group over its ground field is the identity subgroup.