Finiteness of affine group morphisms detected on the kernel

A faithfully flat homomorphism of affine group schemes is finite, of finite type, or of finite presentation exactly when its scheme-theoretic kernel has the corresponding property over the base. No finite-type hypothesis on either ambient group is required, and the base may be any commutative ring.

These criteria reduce finiteness questions about a faithfully flat homomorphism to its kernel over the base. They are useful when the kernel's coordinate algebra is easier to describe than the morphism itself.

In particular, finite presentation of the kernel upgrades an fpqc group homomorphism to an fppf homomorphism, so the fppf first isomorphism theorem applies. The finite criterion detects isogenies among faithfully flat homomorphisms.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §14.
• J. S. Milne, Algebraic Groups (2017), §5.

theorem TauCeti.CommHopfAlgCat.finite_iff_moduleFinite_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) : (↑(CommHopfAlgCat.Hom.hom f)).Finite ↔ Module.Finite R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

A faithfully flat affine group morphism is finite exactly when its scheme-theoretic kernel is finite over the base.

theorem TauCeti.CommHopfAlgCat.finiteType_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : (↑(CommHopfAlgCat.Hom.hom f)).FiniteType) : Algebra.FiniteType R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

The kernel of a finite-type affine group morphism is of finite type over the base.

theorem TauCeti.CommHopfAlgCat.finiteType_iff_finiteType_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) : (↑(CommHopfAlgCat.Hom.hom f)).FiniteType ↔ Algebra.FiniteType R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

A faithfully flat affine group morphism is of finite type exactly when its scheme-theoretic kernel is of finite type over the base.

theorem TauCeti.CommHopfAlgCat.finitePresentation_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : (↑(CommHopfAlgCat.Hom.hom f)).FinitePresentation) : Algebra.FinitePresentation R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

The kernel of a finitely presented affine group morphism is finitely presented over the base.

theorem TauCeti.CommHopfAlgCat.finitePresentation_iff_finitePresentation_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) : (↑(CommHopfAlgCat.Hom.hom f)).FinitePresentation ↔ Algebra.FinitePresentation R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

A faithfully flat affine group morphism is finitely presented exactly when its scheme-theoretic kernel is finitely presented over the base. Thus finite presentation of the kernel suffices for the morphism to be an fppf cover.