Products of reductive affine groups #
The direct product of two reductive affine groups over a field is reductive. After extending scalars to an algebraic closure, a connected normal smooth unipotent subgroup of the product maps to such a subgroup of each factor. Reductivity makes both projection images trivial. Since the two coordinate inclusions generate the tensor-product coordinate algebra, the original subgroup is trivial as well.
The proof uses scheme-theoretic images rather than only algebraic-closure-valued points. This retains normality and is valid in every characteristic.
Main declaration #
TauCeti.reductiveCommHopfAlgProperty.tensorProduct: direct products of reductive finite-type affine groups are reductive.
References #
- J. S. Milne, Algebraic Groups (2017), Section 19.b.
- T. A. Springer, Linear Algebraic Groups, Chapter 8.
theorem
TauCeti.reductiveCommHopfAlgProperty.tensorProduct
{k : Type u}
[Field k]
(H K : FiniteTypeCommHopfAlgCat k)
(hH : reductiveCommHopfAlgProperty k H)
(hK : reductiveCommHopfAlgProperty k K)
:
A direct product of reductive finite-type affine groups is reductive.