Products with a normal closed affine subgroup

Let I and J be Hopf ideals in a commutative Hopf algebra H, with I normal. Conjugation of the subgroup defined by J on the normal subgroup defined by I equips their product scheme with a semidirect-product group structure, for which multiplication into Spec H is a group homomorphism. This file packages the corresponding coordinate Hopf-algebra morphism and defines the product subgroup as its scheme-theoretic image.

This is the multiplication-image object required by the maximal-dimension construction of the unipotent radical. Containment of both factors and normality are proved in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Normal.Product.Properties; connectedness, smoothness, and unipotence of the image remain subsequent steps.

Main declarations

• TauCeti.CommHopfAlgCat.quotientNormalConjugation: conjugation of one quotient subgroup on a normal quotient subgroup.
• TauCeti.CommHopfAlgCat.normalSemidirectProduct: the coordinate Hopf algebra of the resulting semidirect product.
• TauCeti.CommHopfAlgCat.productMapOfNormal: the coordinate morphism dual to multiplication.
• TauCeti.CommHopfAlgCat.productOfNormal: the coordinate Hopf algebra of the product image.
• TauCeti.CommHopfAlgCat.productOfNormalGrpObjInclusion: its categorical closed-subgroup inclusion.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 5.a, 6.a.
• A. Borel, Linear Algebraic Groups, Proposition 14.4.

This advances Layer 5, "The unipotent radical", of the ReductiveGroups roadmap by constructing the multiplication image needed for binary-product closure of connected normal smooth unipotent subgroup candidates.

noncomputable def TauCeti.CommHopfAlgCat.quotientNormalConjugation {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : GrpObj.Action (grpObj (quotient H J)) (grpObj (quotient H I))

Conjugation of a quotient closed subgroup on a normal quotient closed subgroup, viewed as an action of affine group objects.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.CommHopfAlgCat.quotientPointsHom_quotientNormalConjugation_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) (z : ↑(HopfAlgebra.points A)) (g : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) ((grpObjPointsMulEquiv (quotient H I) (Opposite.op A)) ((quotientNormalConjugation H I J hI).act ((grpObjPointsMulEquiv (quotient H J) (Opposite.op A)).symm z) ((grpObjPointsMulEquiv (quotient H I) (Opposite.op A)).symm g))) = (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H J A)) z * (CategoryTheory.ConcreteCategory.hom (quotientPointsHom H I A)) g * ((CategoryTheory.ConcreteCategory.hom (quotientPointsHom H J A)) z)⁻¹

Evaluating quotient normal conjugation on points and including into the ambient group gives conjugation by the included acting point.

noncomputable def TauCeti.CommHopfAlgCat.normalSemidirectProduct {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : CommHopfAlgCat R

The coordinate Hopf algebra of the semidirect product of a normal closed affine subgroup and another closed affine subgroup. Its underlying commutative algebra is (H / I) ⊗[ R ] (H / J), and its Hopf structure records conjugation of the second subgroup on the first.

Equations

• TauCeti.CommHopfAlgCat.normalSemidirectProduct H I J hI = (TauCeti.CommHopfAlgCat.quotientNormalConjugation H I J hI).coordinateHopfAlgebra

noncomputable def TauCeti.CommHopfAlgCat.normalSemidirectProductIso {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : normalSemidirectProduct H I J hI ≅ (quotientNormalConjugation H I J hI).coordinateHopfAlgebra

The canonical comparison between the named normal semidirect product and the coordinate Hopf algebra supplied by the categorical semidirect-product construction.

Equations

• TauCeti.CommHopfAlgCat.normalSemidirectProductIso H I J hI = ⋯.mpr (CategoryTheory.Iso.refl (TauCeti.CommHopfAlgCat.quotientNormalConjugation H I J hI).coordinateHopfAlgebra)

instance TauCeti.CommHopfAlgCat.normalSemidirectProduct_finiteType {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) [Algebra.FiniteType R ↑(quotient H I)] [Algebra.FiniteType R ↑(quotient H J)] : Algebra.FiniteType R ↑(normalSemidirectProduct H I J hI)

The coordinate algebra of the named normal semidirect product is finite type when the coordinate algebras of both factors are finite type.

noncomputable def TauCeti.CommHopfAlgCat.normalSemidirectProductCoordinateInl {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : normalSemidirectProduct H I J hI ⟶ quotient H I

The coordinate morphism representing inclusion of the normal factor in the named normal semidirect product.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.CommHopfAlgCat.normalSemidirectProductCoordinateInr {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : normalSemidirectProduct H I J hI ⟶ quotient H J

The coordinate morphism representing inclusion of the acting factor in the named normal semidirect product.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.CommHopfAlgCat.normalSemidirectProductCoordinateInl_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : normalSemidirectProductCoordinateInl H I J hI = CategoryTheory.CategoryStruct.comp (normalSemidirectProductIso H I J hI).hom (quotientNormalConjugation H I J hI).coordinateInl

The normal-factor coordinate morphism is transported by the canonical comparison.

theorem TauCeti.CommHopfAlgCat.normalSemidirectProductCoordinateInr_def {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : normalSemidirectProductCoordinateInr H I J hI = CategoryTheory.CategoryStruct.comp (normalSemidirectProductIso H I J hI).hom (quotientNormalConjugation H I J hI).coordinateInr

The acting-factor coordinate morphism is transported by the canonical comparison.

noncomputable def TauCeti.CommHopfAlgCat.productMapOfNormal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : H ⟶ normalSemidirectProduct H I J hI

The coordinate Hopf-algebra morphism dual to multiplication from the semidirect product of a normal closed subgroup and another closed subgroup into the ambient affine group.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.CommHopfAlgCat.grpObjMap_productMapOfNormal {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I J : HopfIdeal R ↑H) (hI : I.IsNormal) : let i := quotientGrpObjInclusion H I; let j := quotientGrpObjInclusion H J; have x := ⋯; CategoryTheory.CategoryStruct.comp (grpObjMap (normalSemidirectProductIso H I J hI).hom) (grpObjMap (productMapOfNormal H I J hI)) = (GrpObj.Action.normalSemidirectMul i j).hom.hom

After the canonical comparison, the represented group-object map of productMapOfNormal is normal semidirect multiplication.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.productOfNormal {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) : CommHopfAlgCat k

The coordinate Hopf algebra of the scheme-theoretic multiplication image.

Equations

• TauCeti.CommHopfAlgCat.productOfNormal H I J hI = TauCeti.CommHopfAlgCat.image (TauCeti.CommHopfAlgCat.productMapOfNormal H I J hI)

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.productOfNormalGrpObjInclusion {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) : grpObj (productOfNormal H I J hI) ⟶ grpObj H

The categorical closed-subgroup inclusion of the multiplication image into the ambient affine group.

Equations

• One or more equations did not get rendered due to their size.