Finiteness of a center from its reduction

Let H be a finite-type commutative Hopf algebra over a field. Assuming that the tensor square of the reduced center coordinate algebra is reduced, this file shows that the center is finite once its reduction is finite. The quotient map from the center to its reduction has nilradical kernel; finite type makes that kernel finitely generated, so finiteness lifts through it.

Over an algebraically closed field, the reduced center is finite in particular when its identity component is trivial. This is the algebraic last step in the standard proof that the center of a semisimple affine group is finite: semisimplicity must still be used geometrically to trivialize that identity component.

Main declarations

• moduleFinite_centerCoordinate_of_reducedCenter: a center is finite when its reduction is finite and the tensor square of the reduced center coordinate algebra is reduced.
• moduleFinite_centerCoordinate_of_reducedCenter_identityComponent_eq_augmentation: over an algebraically closed field, a center is finite when its reduction has trivial identity component; no tensor-reducedness hypothesis is needed.

References

• J. S. Milne, Algebraic Groups (2017), §§1.f and 21.10.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §11.4.

theorem TauCeti.FiniteTypeCommHopfAlgCat.moduleFinite_centerCoordinate_of_reducedCenter {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced (TensorProduct k (↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj) ⧸ nilradical ↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj)) (↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj) ⧸ nilradical ↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj)))] [Module.Finite k ↑(CommHopfAlgCat.reducedCenterCoordinateHopfAlgebra H.obj)] : Module.Finite k ↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj)

Assuming that the tensor square of the reduced center coordinate algebra is reduced, a finite-type affine group's center is finite when its reduced center is finite.

theorem TauCeti.FiniteTypeCommHopfAlgCat.moduleFinite_centerCoordinate_of_reducedCenter_identityComponent_eq_augmentation {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) [IsAlgClosed k] (hidentity : HopfAlgebra.identityComponentHopfIdeal = HopfIdeal.augmentation k ↑(CommHopfAlgCat.reducedCenterCoordinateHopfAlgebra H.obj)) : Module.Finite k ↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj)

Over an algebraically closed field, a finite-type affine group's center is finite when the identity component of its reduced center is the trivial subgroup scheme.