The solvable radical and semisimplicity

This file connects the solvable-radical construction to the definition of a semisimple finite-type affine group. Semisimplicity is equivalent to smoothness, geometric connectedness, and triviality of the solvable radical after base change to an algebraic closure.

Main declarations

• semisimpleCommHopfAlgProperty_iff_solvableRadicalDefiningIdeal_baseChange_eq_augmentation: semisimplicity is equivalent to smoothness, geometric connectedness, and triviality of the geometric solvable radical.
• TauCeti.semisimpleCommHopfAlgProperty.solvableRadicalDefiningIdeal_eq_augmentation: the solvable radical over the ground field of a semisimple group is trivial.

References

• J. S. Milne, Algebraic Groups (2017), Sections 6.45--6.46 and 21.10.
• A. Borel, Linear Algebraic Groups, Section 11.21.

The equivalence follows the formal pattern of TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.Reductive.Basic, applied to the existing universal definition of semisimplicity.

This completes the connection between the solvable radical and semisimplicity in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.semisimpleCommHopfAlgProperty_iff_solvableRadicalDefiningIdeal_baseChange_eq_augmentation (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : semisimpleCommHopfAlgProperty k H ↔ Algebra.Smooth k ↑H.obj ∧ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ H.baseChange.solvableRadicalDefiningIdeal = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

A finite-type affine group is semisimple exactly when it is smooth and geometrically connected and its geometric solvable radical is trivial.

theorem TauCeti.semisimpleCommHopfAlgProperty.solvableRadicalDefiningIdeal_eq_augmentation {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) : H.solvableRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj

The solvable radical of a semisimple finite-type affine group over its ground field is the identity subgroup.