Finite homomorphisms with trivial kernel #
A finite homomorphism of affine group schemes with trivial scheme-theoretic kernel is a closed immersion. In Hopf coordinates, its coordinate map is surjective exactly when its kernel Hopf ideal is the augmentation ideal. Testing the kernel on all algebras is essential: injectivity on field-valued points alone would not detect infinitesimal kernels.
The argument uses Mathlib's theorem that a finite ring epimorphism is surjective. This supplies the trivial-kernel criterion for isogenies without assuming smoothness or a field base.
References #
- J. S. Milne, Algebraic Groups (2017), §5.
theorem
TauCeti.CommHopfAlgCat.surjective_iff_kernelHopfIdeal_eq_augmentation
{R : Type u}
[CommRing R]
{H K : CommHopfAlgCat R}
(f : H ⟶ K)
(hf : (↑(CommHopfAlgCat.Hom.hom f)).Finite)
:
A finite affine group homomorphism has trivial scheme-theoretic kernel exactly when it is a closed immersion, expressed as surjectivity of its coordinate map.