Geometric characters determine morphisms to groups of multiplicative type

If an affine group's target is of multiplicative type, a homomorphism to that target is determined by its pullback on geometric characters. Contravariantly, a coordinate Hopf map whose source is of multiplicative type is determined by its map on geometric group-like elements. These elements span after extension to an algebraic closure, and scalar extension detects equality of the original coordinate maps.

Only the target group must be of multiplicative type; the source group need not be of finite type. No perfectness or smoothness hypothesis is needed, so this also applies to nonreduced groups of multiplicative type. The representation-valued formulation retains the Galois action and supplies uniqueness in the character-group classification.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricCharacterMap_injective {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {K : CommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) : Function.Injective CommHopfAlgCat.geometricCharacterMap

A coordinate morphism out of a multiplicative-type Hopf algebra is determined by its action on geometric characters. The target coordinate algebra is arbitrary.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.geometricCharacterRepresentationMap_injective {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} {K : CommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) : Function.Injective CommHopfAlgCat.geometricCharacterRepresentationMap

Equality of the induced Galois-equivariant character maps detects equality of coordinate morphisms out of a multiplicative-type Hopf algebra.