Character groups of groups of multiplicative type

The geometric character group of a finite-type commutative Hopf algebra of multiplicative type is finitely generated. Indeed, the multiplicative-type hypothesis says that the group-like elements span the coordinate algebra after extension to an algebraic closure, and finite type then forces the group of group-like elements to be finitely generated.

Main declarations

• TauCeti.CommHopfAlgCat.exists_geometricCharacterGroup_mulEquiv_of_multiplicativeType: a multiplicative-type character group is equivalent to a finitely generated commutative group.
• TauCeti.CommHopfAlgCat.geometricCharacterGroup_fg_of_multiplicativeType: the geometric character group of a group of multiplicative type is finitely generated.
• TauCeti.CommHopfAlgCat.additiveCharacterGroup_fg_of_multiplicativeType: its additive form is finitely generated.

References

See J. S. Milne, Algebraic Groups (2017), Definition 12.14.

theorem TauCeti.CommHopfAlgCat.exists_geometricCharacterGroup_mulEquiv_of_multiplicativeType {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : multiplicativeTypeCommHopfAlgProperty k H) : ∃ (G : FGCommGrpCat), Nonempty (geometricCharacterGroup H.obj ≃* ↑G)

The geometric character group of a finite-type commutative Hopf algebra of multiplicative type is equivalent to a finitely generated commutative group.

theorem TauCeti.CommHopfAlgCat.geometricCharacterGroup_fg_of_multiplicativeType {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : multiplicativeTypeCommHopfAlgProperty k H) : Group.FG (geometricCharacterGroup H.obj)

The geometric character group of a finite-type commutative Hopf algebra of multiplicative type is finitely generated.

theorem TauCeti.CommHopfAlgCat.additiveCharacterGroup_fg_of_multiplicativeType {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : multiplicativeTypeCommHopfAlgProperty k H) : AddGroup.FG (additiveCharacterGroup H.obj)

The additive character group of a finite-type commutative Hopf algebra of multiplicative type is finitely generated.