Semisimple affine groups are reductive

Every smooth connected normal unipotent closed subgroup of a semisimple affine group has solvable geometric points. It is therefore trivial by semisimplicity, which is precisely the defining normal-subgroup condition for reductivity.

Main declaration

• TauCeti.semisimpleCommHopfAlgProperty.reductive: every semisimple finite-type commutative Hopf algebra is reductive.
• TauCeti.semisimpleToReductiveCommHopfAlgFunctor: the resulting fully faithful inclusion of semisimple coordinate Hopf algebras into reductive ones.

References

• J. S. Milne, Algebraic Groups (2017), Section 21.
• T. A. Springer, Linear Algebraic Groups, Chapter 8.

This is a structural implication in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.semisimpleCommHopfAlgProperty.reductive {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) : reductiveCommHopfAlgProperty k H

Every semisimple finite-type affine group over a field is reductive.

theorem TauCeti.semisimpleCommHopfAlgProperty_le_reductiveCommHopfAlgProperty (k : Type u) [Field k] : semisimpleCommHopfAlgProperty k ≤ reductiveCommHopfAlgProperty k

Semisimplicity is stronger than reductivity for finite-type commutative Hopf algebras.

@[reducible, inline]

noncomputable abbrev TauCeti.semisimpleToReductiveCommHopfAlgFunctor (k : Type u) [Field k] : CategoryTheory.Functor (SemisimpleCommHopfAlgCat k) (ReductiveCommHopfAlgCat k)

The fully faithful inclusion of semisimple finite-type coordinate Hopf algebras into reductive finite-type coordinate Hopf algebras.

Equations

• TauCeti.semisimpleToReductiveCommHopfAlgFunctor k = CategoryTheory.ObjectProperty.ιOfLE ⋯