Geometric reducedness of products of affine groups

The coordinate algebra of a direct product of affine groups is the tensor product of their coordinate algebras. For affine groups of finite type over a field, geometric reducedness is equivalent to smoothness, and smoothness is preserved by products. It follows that the tensor product of two geometrically reduced coordinate Hopf algebras of finite type is geometrically reduced.

Main declarations

• TauCeti.geometricallyReducedCommHopfAlgProperty.tensorProduct: finite-type geometrically reduced affine groups are closed under direct products.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 1.26 and Corollary 1.27.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty.tensorProduct {k : Type u} [Field k] (H K : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↑K] (hH : geometricallyReducedCommHopfAlgProperty k H) (hK : geometricallyReducedCommHopfAlgProperty k K) : geometricallyReducedCommHopfAlgProperty k ↧(TensorProduct k ↑H ↑K)

The tensor product of two finite-type geometrically reduced commutative Hopf algebras is geometrically reduced. Contravariantly, direct products of geometrically reduced affine groups of finite type are geometrically reduced.