Characterization of tori among groups of multiplicative type

A finite-type group of multiplicative type is a torus exactly when it is geometrically connected and geometrically reduced. After passing to an algebraic closure, its coordinate ring is a group algebra. Reducedness and connectedness force the character group to be torsion-free, while finite generation then identifies it with a finite-rank free abelian group.

Main declarations

• TauCeti.splitTorusCommHopfAlgProperty_coordinateRing: the coordinate Hopf algebra of a finitely generated torsion-free commutative group is a split torus.
• iff_multiplicativeType_and_geometricallyConnected_and_geometricallyReduced: a finite-type commutative Hopf algebra over a field is a torus exactly when it is of multiplicative type, geometrically connected, and geometrically reduced.

References

• J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

This completes the intrinsic characterization of tori required by Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap.

theorem TauCeti.splitTorusCommHopfAlgProperty_coordinateRing (K : Type u) [CommRing K] (G : FGCommGrpCat) [IsMulTorsionFree ↑G] : splitTorusCommHopfAlgProperty K (DiagonalizableGroup.coordinateRing K G)

The coordinate Hopf algebra of a finitely generated torsion-free commutative group is a split torus. Such a G is free of some finite rank n, which is then the rank of the split torus.

theorem TauCeti.torusCommHopfAlgProperty.iff_multiplicativeType_and_geometricallyConnected_and_geometricallyReduced (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : torusCommHopfAlgProperty k H ↔ multiplicativeTypeCommHopfAlgProperty k H ∧ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ geometricallyReducedCommHopfAlgProperty k H.obj

A finite-type commutative Hopf algebra over a field is a torus if and only if it is a group of multiplicative type, geometrically connected, and geometrically reduced.