Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Normal.Product.Properties

Containment and normality of normal-subgroup products #

Let I and J be Hopf ideals of a commutative Hopf algebra H. If I is normal, multiplication from the conjugation semidirect product has a scheme-theoretic image in Spec H. This file proves that the image contains the closed subgroups cut out by both I and J. If J is normal as well, then the product image is normal.

Containment is contravariant: the kernel Hopf ideal of the product coordinate map lies below each of I and J. Normality follows by translating simultaneous-conjugation equivariance of semidirect multiplication to coordinate algebras, then applying the general theorem that the kernel of an equivariant coordinate morphism is normal.

These are two of the structural inputs needed to prove binary-product closure of connected normal smooth unipotent closed subgroups. Connectedness and smooth unipotence of the product image are separate steps.

Main declarations #

References #

This advances Layer 5, "The unipotent radical", of the ReductiveGroups roadmap by proving the containment and normality parts of binary-product closure for unipotent-radical candidates.

source
@[simp]
theorem TauCeti.CommHopfAlgCat.productMapOfNormal_comp_coordinateInl {k : Type u} [CommRing k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) :
CategoryTheory.CategoryStruct.comp (productMapOfNormal H I J hI) (normalSemidirectProductCoordinateInl H I J hI) = mkQuotient H I

Multiplication from the conjugation semidirect product restricts on its normal factor to the closed-subgroup quotient morphism.

source
@[simp]
theorem TauCeti.CommHopfAlgCat.productMapOfNormal_comp_coordinateInl_assoc {k : Type u} [CommRing k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) {Z : CommHopfAlgCat k} (h : quotient H I ⟶ Z) :
CategoryTheory.CategoryStruct.comp (productMapOfNormal H I J hI) (CategoryTheory.CategoryStruct.comp (normalSemidirectProductCoordinateInl H I J hI) h) = CategoryTheory.CategoryStruct.comp (mkQuotient H I) h

Multiplication from the conjugation semidirect product restricts on its normal factor to the closed-subgroup quotient morphism.

source
@[simp]
theorem TauCeti.CommHopfAlgCat.productMapOfNormal_comp_coordinateInr {k : Type u} [CommRing k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) :
CategoryTheory.CategoryStruct.comp (productMapOfNormal H I J hI) (normalSemidirectProductCoordinateInr H I J hI) = mkQuotient H J

Multiplication from the conjugation semidirect product restricts on its acting factor to the closed-subgroup quotient morphism.

source
@[simp]
theorem TauCeti.CommHopfAlgCat.productMapOfNormal_comp_coordinateInr_assoc {k : Type u} [CommRing k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) {Z : CommHopfAlgCat k} (h : quotient H J ⟶ Z) :
CategoryTheory.CategoryStruct.comp (productMapOfNormal H I J hI) (CategoryTheory.CategoryStruct.comp (normalSemidirectProductCoordinateInr H I J hI) h) = CategoryTheory.CategoryStruct.comp (mkQuotient H J) h

Multiplication from the conjugation semidirect product restricts on its acting factor to the closed-subgroup quotient morphism.

source
theorem TauCeti.CommHopfAlgCat.ker_productMapOfNormal_le_left {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) :
HopfIdeal.ker (CommHopfAlgCat.Hom.hom (productMapOfNormal H I J hI)) ≤ I

The defining Hopf ideal of the multiplication image lies below the ideal of the normal factor. Equivalently, the product image contains that factor as a closed subgroup scheme.

source
theorem TauCeti.CommHopfAlgCat.ker_productMapOfNormal_le_right {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) :
HopfIdeal.ker (CommHopfAlgCat.Hom.hom (productMapOfNormal H I J hI)) ≤ J

The defining Hopf ideal of the multiplication image lies below the ideal of the acting factor. Equivalently, the product image contains that factor as a closed subgroup scheme.

source
theorem TauCeti.CommHopfAlgCat.isNormal_ker_productMapOfNormal {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) (hJ : J.IsNormal) :
(HopfIdeal.ker (CommHopfAlgCat.Hom.hom (productMapOfNormal H I J hI))).IsNormal

If both factors are normal, the Hopf ideal defining their scheme-theoretic multiplication image is normal. Thus the product image is a normal closed affine subgroup of the ambient group.