Geometric character criterion for isogenies of multiplicative-type groups

On the geometric fibre of a group of multiplicative type, the coordinate Hopf algebra is spanned by its group-like elements. Thus a morphism of two such groups is a central isogeny exactly when its map on geometric characters is injective with finite cokernel. Field-extension descent detects the isogeny over the original field. This applies over an arbitrary ground field and includes nonsmooth groups.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.9.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.isCentralIsogeny_iff_geometricCharacterMap_injective_and_finite_quotient {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) (hK : multiplicativeTypeCommHopfAlgProperty k K) (f : H.obj ⟶ K.obj) : CommHopfAlgCat.IsCentralIsogeny f ↔ Function.Injective ⇑(CommHopfAlgCat.geometricCharacterMap f) ∧ Finite (CommHopfAlgCat.geometricCharacterGroup K.obj ⧸ (CommHopfAlgCat.geometricCharacterMap f).range)

A morphism of multiplicative-type groups is a central isogeny exactly when the induced geometric character map is injective with finite cokernel.