Reductivity over an algebraically closed field

Over an algebraically closed field, reductivity can be tested by the unipotent radical over the ground field. An algebraic closure of an algebraically closed field is a trivial extension, so its Hopf ideals descend, together with normality, connectedness and smooth unipotence. Consequently the geometric fibre of a reductive group is itself reductive. This lets results over algebraically closed fields be applied to the geometric fibre and then descended.

The subgroup descent uses CommHopfAlgCat.baseChangeHopfIdeal_surjective and the existing normality and geometric-connectedness descent APIs.

References

• J. S. Milne, Algebraic Groups (2017), Chapters 6 and 19.

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

Over an algebraically closed field, reductivity is equivalent to smoothness, geometric connectedness and triviality of the unipotent radical over the ground field.

theorem TauCeti.reductiveCommHopfAlgProperty.algebraicClosureBaseChange {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) : reductiveCommHopfAlgProperty (AlgebraicClosure k) H.baseChange

The geometric fibre of a reductive affine group is reductive.