Descent of finiteness of the center

A field extension preserves and reflects finiteness of the scheme-theoretic center of an affine group. Thus finiteness may be proved over an algebraic closure and then descended to the original field, as in the finite-center theorem for semisimple groups. No smoothness, connectedness, or finite-type assumption on the ambient group is needed for this descent.

The coordinate comparison is CommHopfAlgCat.centerCoordinateBaseChangeIso. Finiteness of its tensor-product side descends by Mathlib's Module.Finite.of_finite_tensorProduct_of_faithfullyFlat.

@[simp]

theorem TauCeti.CommHopfAlgCat.moduleFinite_centerCoordinate_baseChange_iff {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : Module.Finite K ↑(centerCoordinateHopfAlgebra (baseChange H)) ↔ Module.Finite k ↑(centerCoordinateHopfAlgebra H)

A field extension preserves and reflects finiteness of the full scheme-theoretic center, including any non-reduced structure.