Central isogenies between diagonalizable coordinate algebras

For diagonalizable coordinate Hopf algebras over a domain with torsion-free carriers, a morphism is a central isogeny precisely when its map on group-like elements is injective with finite cokernel. The group-like elements give the intrinsic character groups; no presentation as a group algebra needs to be chosen. This form applies to geometric fibres of groups of multiplicative type, where the defining character group is available only after scalar extension.

References

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

@[simp]

theorem TauCeti.DiagonalizableGroup.isCentralIsogeny_iff_groupLikeMap_injective_and_finite_quotient {k : Type u} [CommRing k] [IsDomain k] {H K : CommHopfAlgCat k} [Module.IsTorsionFree k ↑H] [Module.IsTorsionFree k ↑K] (hH : Submodule.span k (Set.range GroupLike.val) = ⊤) (hK : Submodule.span k (Set.range GroupLike.val) = ⊤) (f : H ⟶ K) : CommHopfAlgCat.IsCentralIsogeny f ↔ Function.Injective ⇑(GroupLike.map (CommHopfAlgCat.Hom.hom f)) ∧ Finite (GroupLike k ↑K ⧸ (GroupLike.map (CommHopfAlgCat.Hom.hom f)).range)

A morphism between torsion-free diagonalizable coordinate algebras over a domain is a central isogeny exactly when its intrinsic character map is injective with finite cokernel.