Smoothness of products of affine groups

The coordinate algebra of a direct or semidirect product of affine groups is the tensor product of the two coordinate algebras. Smoothness is preserved by base change and composition, so the product is smooth when both factors are. Smoothness then descends to a scheme-theoretic image in a finite-type ambient affine group.

Main declarations

• TauCeti.smoothCommHopfAlgProperty.tensorProduct: a direct product of smooth affine groups is smooth.
• TauCeti.smoothCommHopfAlgProperty.semidirectProduct: a semidirect product of smooth affine groups is smooth.
• TauCeti.smoothCommHopfAlgProperty.normalSemidirectProduct: the conjugation semidirect-product source associated to two smooth closed subgroups is smooth.
• TauCeti.smoothCommHopfAlgProperty.productOfNormal: the multiplication image of a normal smooth subgroup and another smooth subgroup is smooth in a finite-type ambient affine group.

This supplies the smoothness part of binary-product closure in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.

theorem TauCeti.smoothCommHopfAlgProperty.tensorProduct {R : Type u} [CommRing R] (H K : CommHopfAlgCat R) (hH : smoothCommHopfAlgProperty R H) (hK : smoothCommHopfAlgProperty R K) : smoothCommHopfAlgProperty R ↧(TensorProduct R ↑H ↑K)

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

theorem TauCeti.smoothCommHopfAlgProperty.semidirectProduct {R : Type u} [CommRing R] (H K : CommHopfAlgCat R) (A : GrpObj.Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) (hH : smoothCommHopfAlgProperty R H) (hK : smoothCommHopfAlgProperty R K) : smoothCommHopfAlgProperty R A.coordinateHopfAlgebra

The semidirect product associated to an action of smooth affine groups is smooth.

theorem TauCeti.smoothCommHopfAlgProperty.normalSemidirectProduct {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) (hIs : smoothCommHopfAlgProperty R (CommHopfAlgCat.quotient H I)) (hJs : smoothCommHopfAlgProperty R (CommHopfAlgCat.quotient H J)) : smoothCommHopfAlgProperty R (CommHopfAlgCat.normalSemidirectProduct H I J hI)

The conjugation semidirect-product source associated to a normal smooth closed subgroup and another smooth closed subgroup is smooth.

theorem TauCeti.smoothCommHopfAlgProperty.productOfNormal {k : Type u} [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (I J : HopfIdeal k ↑H) (hI : I.IsNormal) (hIs : smoothCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)) (hJs : smoothCommHopfAlgProperty k (CommHopfAlgCat.quotient H J)) : smoothCommHopfAlgProperty k (CommHopfAlgCat.productOfNormal H I J hI)

The scheme-theoretic multiplication image of a normal smooth closed affine subgroup and another smooth closed affine subgroup is smooth when the ambient affine group is finite type.