Normal closed subgroups generated by morphisms

Let f i : H ⟶ K i be morphisms of commutative Hopf algebras. The ordinary common-kernel construction takes the largest Hopf ideal killed by every f i; contravariantly, its quotient is the smallest closed subgroup scheme of Spec H containing all the images. This file adds the normal version: take the supremum only over normal Hopf ideals killed by every f i.

The resulting quotient represents the smallest normal closed subgroup scheme containing the family. It comes with its universal property, factorization maps to every K i, and a comparison with the ordinary generated subgroup. If the ordinary common-kernel ideal is already normal, the normal and ordinary generated subgroups agree.

Main declarations

• TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal: the largest normal Hopf ideal killed by a family of morphisms.
• TauCeti.CommHopfAlgCat.isNormal_normalCommonKernelHopfIdeal: the ideal is normal.
• TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal_le_commonKernelHopfIdeal: comparison with the ordinary common-kernel ideal.
• TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal_eq_commonKernelHopfIdeal_of_isNormal: agreement when the ordinary common-kernel ideal is normal.
• TauCeti.CommHopfAlgCat.le_normalCommonKernelHopfIdeal_iff_of_isNormal: its universal property.
• TauCeti.CommHopfAlgCat.normalCommonKernelLift: the induced factorization through the normal generated subgroup.
• TauCeti.CommHopfAlgCat.normalCommonKernelLift_unique: uniqueness of that factorization.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §§15--16.

This is subgroup-generation infrastructure for Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. The radical construction must form a normal closed subgroup containing all connected normal unipotent candidates before proving that the generated subgroup remains connected and unipotent.

noncomputable def TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) : HopfIdeal R ↑H

The largest normal Hopf ideal of H contained in the kernels of every morphism in f.

Contravariantly, quotienting by this ideal gives the smallest normal closed subgroup scheme of Spec H through which all the morphisms Spec (K i) ⟶ Spec H factor.

Equations

• TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal f = (TauCeti.CommHopfAlgCat.commonKernelHopfIdeal f).normalCore

@[simp]

theorem TauCeti.CommHopfAlgCat.isNormal_normalCommonKernelHopfIdeal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) : (normalCommonKernelHopfIdeal f).IsNormal

The normal common-kernel ideal is normal.

theorem TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal_le_commonKernelHopfIdeal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) : normalCommonKernelHopfIdeal f ≤ commonKernelHopfIdeal f

The normal common-kernel ideal lies below the ordinary common-kernel ideal.

theorem TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal_eq_commonKernelHopfIdeal_of_isNormal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (h : (commonKernelHopfIdeal f).IsNormal) : normalCommonKernelHopfIdeal f = commonKernelHopfIdeal f

If the ordinary common-kernel ideal is normal, it agrees with the normal common-kernel ideal.

theorem TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal_toIdeal_le_ker {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (i : ι) : (normalCommonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (f i))).toRingHom

Every member of the defining family kills the normal common-kernel ideal.

theorem TauCeti.CommHopfAlgCat.le_normalCommonKernelHopfIdeal_iff_of_isNormal {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : I ≤ normalCommonKernelHopfIdeal f ↔ ∀ (i : ι), I.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (f i))).toRingHom

A normal Hopf ideal lies below the normal common-kernel ideal exactly when every member of the family kills it.

noncomputable def TauCeti.CommHopfAlgCat.normalCommonKernelLift {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (i : ι) : quotient H (normalCommonKernelHopfIdeal f) ⟶ K i

The morphism from the normal common-kernel quotient induced by the ith member of the family.

Equations

• TauCeti.CommHopfAlgCat.normalCommonKernelLift f i = TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.CommHopfAlgCat.normalCommonKernelHopfIdeal f) (f i) ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_normalCommonKernelLift {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (i : ι) : CategoryTheory.CategoryStruct.comp (mkQuotient H (normalCommonKernelHopfIdeal f)) (normalCommonKernelLift f i) = f i

The quotient morphism followed by the normal common-kernel lift is the original morphism.

theorem TauCeti.CommHopfAlgCat.normalCommonKernelLift_unique {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (i : ι) (g : quotient H (normalCommonKernelHopfIdeal f) ⟶ K i) (hg : CategoryTheory.CategoryStruct.comp (mkQuotient H (normalCommonKernelHopfIdeal f)) g = f i) : g = normalCommonKernelLift f i

A morphism from the normal common-kernel quotient is determined by its composite with the quotient morphism.

theorem TauCeti.CommHopfAlgCat.normalCommonKernelLift_surjective_of_surjective {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (i : ι) (hi : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (f i))) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (normalCommonKernelLift f i))

A surjective member of the family remains surjective after factoring through the normal generated subgroup.