Endomorphisms of a subgroup scheme generated by a family of morphisms

Let f i : H ⟶ K i be morphisms of commutative Hopf algebras and let 𝔞 be their common-kernel Hopf ideal, the largest Hopf ideal of H killed by all of them. Contravariantly, Spec (H ⧸ 𝔞) is the closed subgroup scheme of Spec H generated by the images of the Spec (K i), and a morphism of commutative Hopf algebras ψ : H ⟶ H ⧸ 𝔞 is a homomorphism from that subgroup scheme to Spec H.

Such a homomorphism maps the generated subgroup scheme into itself exactly when ψ is killed by 𝔞, and this file reduces that condition to the generators: it suffices that each composite of ψ with a factored generator is killed by 𝔞, which holds as soon as each generator is carried into some generator.

The reduction is the two-sided argument for 𝔞. The image Hopf ideal ψ(𝔞) of H ⧸ 𝔞 pulls back along the quotient morphism to a Hopf ideal of H containing 𝔞; the generator equations make every f i kill that pullback, so it is contained in 𝔞 because 𝔞 is the largest Hopf ideal with that property. The pullback is therefore 𝔞 itself, and ψ(𝔞) is zero. Contravariantly: the preimage of the generated subgroup scheme under the homomorphism is a closed subgroup scheme containing every generator, hence the whole of it.

From that containment the homomorphism factors through the generated subgroup scheme, giving an endomorphism of it as a group scheme. Two such endomorphisms whose coordinate morphisms agree on the generators are equal, by rigidity.

Nothing here asserts that such an endomorphism is an isogeny, surjective, or flat.

Main results

In the namespace TauCeti.CommHopfAlgCat:

• commonKernelHopfIdeal_toIdeal_le_ker_of_comp_commonKernelLift and commonKernelHopfIdeal_toIdeal_le_ker_of_comp_eq: the coordinate morphism is killed by the common-kernel ideal, from kernel containments and from generator equations respectively.
• commonKernelSpecRestrict, commonKernelSpecRestrict_comp_quotientSpecι and commonKernelSpecRestrict_eq_of_comp_eq: the resulting endomorphism of the generated subgroup scheme, its compatibility with the closed immersion, and its determination by the generators.

References

• R. W. Carter, Simple Groups of Lie Type, §§7.1 and 12.2, for endomorphisms of a Chevalley group determined by their effect on the root subgroups and the torus.
• J. E. Humphreys, Linear Algebraic Groups, §27.
• J. C. Jantzen, Representations of Algebraic Groups, I.2, for the Hopf-ideal dictionary used in the reduction.

theorem TauCeti.CommHopfAlgCat.commonKernelHopfIdeal_toIdeal_le_ker_of_comp_commonKernelLift {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (ψ : H ⟶ quotient H (commonKernelHopfIdeal f)) (hgen : ∀ (i : ι), (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp ψ (commonKernelLift f i)))).toRingHom) : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom

A morphism into the common-kernel quotient whose composites with the factored generators are killed by the common-kernel ideal is itself killed by it. Contravariantly, a homomorphism from the generated closed subgroup scheme to the ambient one which carries every generating subgroup back into it maps the whole subgroup scheme into it.

theorem TauCeti.CommHopfAlgCat.commonKernelHopfIdeal_toIdeal_le_ker_of_comp_eq {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} (f : (i : ι) → H ⟶ K i) (ψ : H ⟶ quotient H (commonKernelHopfIdeal f)) (s : ι → ι) (m : (i : ι) → K (s i) ⟶ K i) (hgen : ∀ (i : ι), CategoryTheory.CategoryStruct.comp ψ (commonKernelLift f i) = CategoryTheory.CategoryStruct.comp (f (s i)) (m i)) : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom

The generator form of the previous criterion. A morphism into the common-kernel quotient whose composite with the ith factored generator is the s ith generator followed by a morphism m i of the codomains is killed by the common-kernel ideal.

Contravariantly, this is a homomorphism from the generated subgroup scheme to the ambient one which sends the ith generating subgroup into the s ith one.

The restricted endomorphism

noncomputable def TauCeti.CommHopfAlgCat.commonKernelSpecRestrict {R : Type u} [CommRing R] {ι : Type w} {H : CommHopfAlgCat R} {K : ι → CommHopfAlgCat R} {f : (i : ι) → H ⟶ K i} (ψ : H ⟶ quotient H (commonKernelHopfIdeal f)) (hψ : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) : quotientSpec H (commonKernelHopfIdeal f) ⟶ quotientSpec H (commonKernelHopfIdeal f)

The endomorphism of a generated closed subgroup scheme restricting a homomorphism into the ambient group scheme which maps it into itself: the spectrum of the factorization of the coordinate morphism ψ through the common-kernel quotient.

Equations

• TauCeti.CommHopfAlgCat.commonKernelSpecRestrict ψ hψ = (AlgebraicGeometry.hopfSpec ↧R).map (TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.CommHopfAlgCat.commonKernelHopfIdeal f) ψ hψ).op

theorem TauCeti.CommHopfAlgCat.commonKernelSpecRestrict_def {R : Type u} [CommRing R] {ι : Type w} {H : CommHopfAlgCat R} {K : ι → CommHopfAlgCat R} {f : (i : ι) → H ⟶ K i} (ψ : H ⟶ quotient H (commonKernelHopfIdeal f)) (hψ : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) : commonKernelSpecRestrict ψ hψ = (AlgebraicGeometry.hopfSpec ↧R).map (liftQuotient (commonKernelHopfIdeal f) ψ hψ).op

The restricted endomorphism is the spectrum of the quotient factorization.

@[simp]

theorem TauCeti.CommHopfAlgCat.commonKernelSpecRestrict_comp_quotientSpecι {R : Type u} [CommRing R] {ι : Type w} {H : CommHopfAlgCat R} {K : ι → CommHopfAlgCat R} {f : (i : ι) → H ⟶ K i} (ψ : H ⟶ quotient H (commonKernelHopfIdeal f)) (hψ : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) : CategoryTheory.CategoryStruct.comp (commonKernelSpecRestrict ψ hψ) (quotientSpecι H (commonKernelHopfIdeal f)) = (AlgebraicGeometry.hopfSpec ↧R).map ψ.op

Following the restricted endomorphism by the closed immersion into the ambient group scheme recovers the original homomorphism.

theorem TauCeti.CommHopfAlgCat.commonKernelSpecRestrict_eq_of_comp_eq {R : Type u} [CommRing R] {ι : Type w} {H : CommHopfAlgCat R} {K : ι → CommHopfAlgCat R} {f : (i : ι) → H ⟶ K i} (ψ ψ' : H ⟶ quotient H (commonKernelHopfIdeal f)) (hψ : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) (hψ' : (commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ')).toRingHom) (hgen : ∀ (i : ι), CategoryTheory.CategoryStruct.comp ψ (commonKernelLift f i) = CategoryTheory.CategoryStruct.comp ψ' (commonKernelLift f i)) : commonKernelSpecRestrict ψ hψ = commonKernelSpecRestrict ψ' hψ'

Two restricted endomorphisms agreeing on the generators agree. The coordinate morphisms are determined by their composites with the factored generators, so the endomorphisms they restrict to are equal.