Finite algebraic splitting fields for groups of multiplicative type

Every finite-type affine group of multiplicative type becomes diagonalizable over a finite intermediate field of an algebraic closure. This is a field of definition for all of its geometric characters, obtained from finitely many character generators. The result does not assert that the extension is separable, and requires neither perfectness nor smoothness.

References

• J. S. Milne, Algebraic Groups (2017), §12.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty.exists_finiteDimensional_groupLikeSpanned_baseChange {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : multiplicativeTypeCommHopfAlgProperty k H) : ∃ (L : IntermediateField k (AlgebraicClosure k)), FiniteDimensional k ↥L ∧ DiagonalizableGroup.groupLikeSpannedProperty (↥L) H.baseChange

Every finite-type group of multiplicative type is diagonalizable over a finite algebraic extension.