Finite fields of definition for characters

If the characters of a Hopf algebra over an algebraic extension form a finitely generated group, then they are all defined over one finite intermediate field. If these characters also span the extended algebra, they span over that finite field already. This supplies finite algebraic splitting fields for affine groups of multiplicative type.

References

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

theorem TauCeti.exists_finiteDimensional_surjective_groupLikeScalarTowerHom {k : Type u_1} {K : Type u_2} {A : Type u_3} [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] [Ring A] [HopfAlgebra k A] [Group.FG (GroupLike K (TensorProduct k K A))] : ∃ (L : IntermediateField k K), FiniteDimensional k ↥L ∧ Function.Surjective ⇑groupLikeScalarTowerHom

A finitely generated character group over an algebraic extension is defined over a common finite intermediate field.

theorem TauCeti.exists_finiteDimensional_span_groupLike_eq_top {k : Type u_1} {K : Type u_2} {A : Type u_3} [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] [Ring A] [HopfAlgebra k A] [Group.FG (GroupLike K (TensorProduct k K A))] (hspan : Submodule.span K (Set.range GroupLike.val) = ⊤) : ∃ (L : IntermediateField k K), FiniteDimensional k ↥L ∧ Submodule.span (↥L) (Set.range GroupLike.val) = ⊤

If finitely generated characters span after an algebraic extension, they already span after a finite intermediate extension.