Groups of multiplicative type are linearly reductive

An affine group of multiplicative type over a field k becomes diagonalizable over the algebraic closure AlgebraicClosure k, where its coordinate Hopf algebra is a group algebra. Comodules over a group algebra are completely reducible, being direct sums of their weight spaces, and complete reducibility descends from any extension field back to k. Hence every group of multiplicative type, and in particular every torus, split or not, is linearly reductive over its base field.

This is the easy implication of the characterization of linearly reductive groups in positive characteristic: over an algebraically closed field of characteristic p, a smooth connected affine group is linearly reductive exactly when it is a torus.

Main declarations

• TauCeti.multiplicativeTypeCommHopfAlgProperty.linearlyReductive: a finite-type commutative Hopf algebra of multiplicative type is linearly reductive.
• TauCeti.torusCommHopfAlgProperty.linearlyReductive: the coordinate Hopf algebra of a torus is linearly reductive.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.30.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 3.2.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.linearlyReductive {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) : linearlyReductiveCommHopfAlgProperty k H.obj

Groups of multiplicative type are linearly reductive. A finite-type commutative Hopf algebra over a field that becomes diagonalizable over an algebraic closure is linearly reductive.

theorem TauCeti.torusCommHopfAlgProperty.linearlyReductive {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : torusCommHopfAlgProperty k H) : linearlyReductiveCommHopfAlgProperty k H.obj

Tori are linearly reductive. The coordinate Hopf algebra of a torus over a field, split or not, is linearly reductive.