Geometric solvability under field extension

Let H be a finite-type commutative Hopf algebra over a field k, and let K / k be any field extension. Geometric solvability of the affine group represented by H is equivalent to geometric solvability after extending scalars to K.

Preservation under scalar extension is proved in TauCeti.Algebra.AlgebraicGroup.Solvable.Reduced: finite-type point separation turns solvability into a universal derived-word identity, which remains valid over K. This file proves reflection. Choose a k-embedding of AlgebraicClosure k into AlgebraicClosure K. Postcomposition embeds the original geometric point group into the points valued in AlgebraicClosure K, and the standard base-change equivalence identifies the latter with the geometric point group of K ⊗[k] H. Solvability passes to subgroups, giving the result.

Main declarations

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.of_baseChange: geometric solvability is reflected by arbitrary field extension.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.baseChange_iff: geometric solvability is invariant under arbitrary field extension for finite-type affine groups.

References

• J. S. Milne, Algebraic Groups (2017), §§6.45--6.46.
• A. Borel, Linear Algebraic Groups, §11.21.

This supplies the two-way scalar-extension interface needed to compare solvable radicals in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.of_baseChange {k : Type u} [Field k] {K : Type w} [Field K] [Algebra k K] (H : CommHopfAlgCat k) (hH : geometricallySolvablePointsCommHopfAlgProperty K (CommHopfAlgCat.baseChange H)) : geometricallySolvablePointsCommHopfAlgProperty k H

Geometric solvability is reflected by arbitrary field extension.

The point group over AlgebraicClosure k embeds into the point group over AlgebraicClosure K, which is identified with the geometric points of the base-changed Hopf algebra.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.baseChange_iff {k : Type u} [Field k] {K : Type w} [Field K] [Algebra k K] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : geometricallySolvablePointsCommHopfAlgProperty K (CommHopfAlgCat.baseChange H) ↔ geometricallySolvablePointsCommHopfAlgProperty k H

Geometric solvability of a finite-type affine group is invariant under arbitrary extension of the ground field.