Geometrically linearly reductive affine group schemes are reductive

This module transfers the implication from geometric linear reductivity to reductivity from coordinate Hopf algebras to finite-type affine group schemes. The hypothesis says that the coordinate Hopf algebra after scalar extension to an algebraic closure has completely reducible finite-dimensional comodules. Together with smoothness and geometric connectedness, this rules out nontrivial geometric unipotent normal subgroups, hence gives reductivity.

Main declaration

• TauCeti.reductiveAffineGroupSchemeProperty. of_smooth_of_geometricallyConnected_of_coordinateBaseChange_linearlyReductive: a smooth geometrically connected finite-type affine group scheme is reductive when the coordinate Hopf algebra of its geometric fibre is linearly reductive.

References

• J. S. Milne, Algebraic Groups (2017), Corollary 12.45 and §22.42.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Sections 3.2 and 8.3.

The argument is the scheme-side form of the comparison between reductivity and complete reducibility in the theory of affine algebraic groups.

theorem TauCeti.reductiveAffineGroupSchemeProperty.of_smooth_of_geometricallyConnected_of_coordinateBaseChange_linearlyReductive (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hsm : AlgebraicGeometry.Smooth G.obj.obj.X.hom) (hconn : AlgebraicGeometry.GeometricallyConnected G.obj.obj.X.hom) (hlr : linearlyReductiveCommHopfAlgProperty (AlgebraicClosure k) (Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G)).baseChange.obj) : reductiveAffineGroupSchemeProperty k G

A smooth geometrically connected finite-type affine group scheme is reductive when the coordinate Hopf algebra of its geometric fibre is linearly reductive.