Complete reducibility for reductive affine groups

Over a field of characteristic zero, every finite-dimensional rational representation of a reductive affine group is completely reducible. After extension to an algebraic closure, the Lie algebra has central radical, and its center acts semisimply because it comes from the radical torus of the group. Complete reducibility for reductive Lie algebras therefore applies to the differentiated representation. Connectedness identifies Lie-stable subspaces with subrepresentations, so the complements are rational subrepresentations. Linear reductivity descends from the algebraic closure to the original field. Together with the converse for smooth geometrically connected groups, this gives the equivalence between reductivity and linear reductivity in characteristic zero. Every rational representation, including an infinite-dimensional one, is therefore completely reducible.

The Lie-algebra inputs are reductiveCommHopfAlgProperty.hasCentralRadical_lieAlgebra and reductiveCommHopfAlgProperty.isSemisimple_differential_of_mem_center. The passage back to comodules uses Comodule.isCompletelyReducible_iff_forall_differential_mem. The differentiated Lie action is assembled as in TauCeti.Algebra.AlgebraicGroup.Representation.CompleteReducibility.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 22.
• J. E. Humphreys, Linear Algebraic Groups, §13.
• TauCeti.Algebra.Lie.Reductive.CompleteReducibility, for complete reducibility with semisimple central action.

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

A reductive affine group over any field of characteristic zero is linearly reductive. Neither algebraic closedness nor a splitting hypothesis is required.

theorem TauCeti.Comodule.isCompletelyReducible_of_reductive {k : Type u} [Field k] [CharZero k] {H : FiniteTypeCommHopfAlgCat k} (hH : reductiveCommHopfAlgProperty k H) {M : Type w} [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] : IsCompletelyReducible k (↑H.obj) M

Every rational representation of a reductive affine group in characteristic zero is completely reducible over the original field, without a finite-dimensionality assumption.

theorem TauCeti.reductiveCommHopfAlgProperty_iff_linearlyReductive {k : Type u} [Field k] [CharZero k] (H : FiniteTypeCommHopfAlgCat k) (hconnected : geometricallyConnectedCommHopfAlgProperty k H.obj) : reductiveCommHopfAlgProperty k H ↔ linearlyReductiveCommHopfAlgProperty k H.obj

For geometrically connected affine groups in characteristic zero, reductivity and complete reducibility of all finite-dimensional rational representations are equivalent. Smoothness is automatic by Cartier's theorem.