Complete reducibility from a semisimple Lie algebra in characteristic zero

Let G be a connected affine group of finite type over an algebraically closed field k of characteristic zero. If the Lie algebra Lie(G) has nondegenerate Killing form, equivalently (by Cartan's criterion) Lie(G) is semisimple, then every finite-dimensional representation of G is completely reducible, so G is linearly reductive.

A representation M of G differentiates to a representation of Lie(G). By Weyl's complete reducibility theorem every Lie(G)-submodule of M has a Lie(G)-stable complement. In characteristic zero, for connected G, the Lie(G)-stable subspaces of M are exactly its subrepresentations, so these complements are subrepresentations. Connectedness is used only in that identification; characteristic zero is used there, through Cartier's theorem, and in Weyl's theorem.

Over an arbitrary field of characteristic zero the same holds for geometrically connected G: nondegeneracy of the Killing form survives extension to an algebraic closure, and linear reductivity descends from it.

Main declarations

• TauCeti.Comodule.isCompletelyReducible_of_isKilling: over an algebraically closed field, a finite-dimensional representation of a connected group whose Lie algebra has nondegenerate Killing form is completely reducible.
• TauCeti.Coalgebra.isLinearlyReductive_of_isKilling and TauCeti.linearlyReductiveCommHopfAlgProperty.of_isKilling: such a group is linearly reductive.
• TauCeti.linearlyReductiveCommHopfAlgProperty.of_geometricallyConnected_of_isKilling: over any field of characteristic zero, a geometrically connected finite-type affine group whose Lie algebra has nondegenerate Killing form is linearly reductive.

References

• J. S. Milne, Algebraic Groups (2017), §22.42.
• J. E. Humphreys, Linear Algebraic Groups, §13 (characteristic zero theory).
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §6.3, for Weyl's theorem.

theorem TauCeti.Comodule.isCompletelyReducible_of_isKilling {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsKilling k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] {M : Type w} [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] : IsCompletelyReducible k (↑H.obj) M

Weyl's theorem for algebraic groups. Over an algebraically closed field of characteristic zero, every finite-dimensional representation of a connected group whose Lie algebra has nondegenerate Killing form is completely reducible.

theorem TauCeti.Coalgebra.isLinearlyReductive_of_isKilling {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsKilling k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] : IsLinearlyReductive k ↑H.obj

Over an algebraically closed field of characteristic zero, a connected group whose Lie algebra has nondegenerate Killing form is linearly reductive, with comodule carriers in any universe.

theorem TauCeti.linearlyReductiveCommHopfAlgProperty.of_isKilling {k : Type u} [Field k] [CharZero k] [IsAlgClosed k] {H : FiniteTypeCommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑H.obj)] [LieAlgebra.IsKilling k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] : linearlyReductiveCommHopfAlgProperty k H.obj

Over an algebraically closed field of characteristic zero, the coordinate Hopf algebra of a connected group whose Lie algebra has nondegenerate Killing form is linearly reductive.

theorem TauCeti.linearlyReductiveCommHopfAlgProperty.of_geometricallyConnected_of_isKilling {k : Type u} [Field k] [CharZero k] {H : FiniteTypeCommHopfAlgCat k} [LieAlgebra.IsKilling k (Derivation k (↑H.obj) (Bialgebra.CounitAlgebra k (↑H.obj) k))] (hH : geometricallyConnectedCommHopfAlgProperty k H.obj) : linearlyReductiveCommHopfAlgProperty k H.obj

Lie-semisimple groups are linearly reductive in characteristic zero. Over a field of characteristic zero, a geometrically connected finite-type affine group whose Lie algebra has nondegenerate Killing form is linearly reductive.