Products of smooth unipotent affine groups

The tensor product of two commutative Hopf algebras is the coordinate algebra of the direct product of their affine group schemes. This file proves that the representation-theoretic unipotence condition is preserved and reflected by this product.

For points g and h of the two factors, the corresponding product point factors as

(g, h) = (g, 1) * (1, h).

The two factors commute. Each is unipotent because it is obtained from g or h by precomposition with the bialgebra projection that applies the counit to the other tensor factor. Thus their product is unipotent. Conversely, the two components of a unipotent product point are unipotent by precomposition with the coordinate inclusions.

Combining this pointwise result with stability of smoothness and finite type under tensor products shows that direct products of smooth unipotent affine groups are smooth unipotent.

Main declarations

• TauCeti.HopfAlgebra.isUnipotentPoint_pointsMulEquiv_iff: a product point is unipotent exactly when both of its components are.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.tensorProduct: geometric-point unipotence is closed under products.
• TauCeti.smoothUnipotentCommHopfAlgProperty.tensorProduct: smooth unipotent finite-type affine groups are closed under products.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.

This advances Layer 5, "Unipotent groups", of the ReductiveGroups roadmap by establishing the basic product closure needed to assemble unipotent groups from simpler factors.

theorem TauCeti.HopfAlgebra.isUnipotentPoint_pointsMulEquiv_iff {k : Type u} [CommSemiring k] {H K : Type v} [CommSemiring H] [CommSemiring K] [HopfAlgebra k H] [HopfAlgebra k K] {A : Type w} [CommRing A] [Algebra k A] (g : WithConv (TensorProduct k H K →ₐ[k] A)) : IsUnipotentPoint g ↔ IsUnipotentPoint (AffineGroup.Product.pointsMulEquiv g).1 ∧ IsUnipotentPoint (AffineGroup.Product.pointsMulEquiv g).2

A point of a product affine group is unipotent exactly when both factor points are unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.tensorProduct (k : Type u) [Field k] (H K : CommHopfAlgCat k) (hH : geometricallyUnipotentPointsCommHopfAlgProperty k H) (hK : geometricallyUnipotentPointsCommHopfAlgProperty k K) : geometricallyUnipotentPointsCommHopfAlgProperty k ↧(TensorProduct k ↑H ↑K)

The tensor product of two coordinate Hopf algebras with unipotent geometric points again has only unipotent geometric points. Contravariantly, geometric-point unipotence is closed under direct products of affine groups.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty.tensorProduct (k : Type u) [Field k] (H K : FiniteTypeCommHopfAlgCat k) (hH : smoothUnipotentCommHopfAlgProperty k H) (hK : smoothUnipotentCommHopfAlgProperty k K) : smoothUnipotentCommHopfAlgProperty k (H.tensorProduct K)

The tensor product of two smooth unipotent finite-type coordinate Hopf algebras is smooth unipotent. Contravariantly, direct products of smooth unipotent affine groups are smooth unipotent.