Geometric solvability, dense morphisms, and base change

An injective morphism f : H ⟶ K of coordinate Hopf algebras represents a schematically dense homomorphism Spec K ⟶ Spec H of affine groups. If K is smooth over the field k, then it is finite type, and solvability of the geometric points of K descends to H.

The proof turns a derived-word identity into a polynomial identity. The value algebra of the universal depth-n derived word is built by repeatedly tensoring K with itself. Smoothness makes this algebra reduced, so algebraic-closure-valued points separate its elements. Injectivity of f, and hence of all its iterated tensor powers, then reflects the universal identity from K to H.

For a finite-type affine group, the same argument makes each coordinate of the universal derived-word defect nilpotent. Every field-valued point kills that defect, proving that geometric solvability survives arbitrary field extension without a smoothness hypothesis.

Main declarations

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.of_injective_of_smooth: geometric solvability descends along an injective coordinate morphism with smooth codomain.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.baseChange: geometric solvability of a finite-type affine group is preserved by field extension.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Section 2.4.

These results supply the image-solvability and scalar-extension steps for the solvable radical in Layer 6 of the ReductiveGroups roadmap.

The following universal-word construction is private proof machinery for the descent theorem. Its public interface is deliberately the theorem at the end of the file.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.of_injective_of_smooth {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) (hK_smooth : Algebra.Smooth k ↑K) (hK : geometricallySolvablePointsCommHopfAlgProperty k K) : geometricallySolvablePointsCommHopfAlgProperty k H

Geometric solvability descends along an injective morphism of coordinate Hopf algebras whose codomain is smooth.

Contravariantly, the morphism represents a schematically dense homomorphism from Spec K to Spec H. A derived-word identity on the algebraic-closure-valued points of K holds in the universal iterated tensor product by point separation, and injectivity reflects that identity to H.

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

Geometric solvability of a finite-type affine group is preserved by arbitrary field extension.

Finite-type Nullstellensatz makes the coordinates of a universal derived-word defect nilpotent. They vanish under points valued in the algebraic closure of the larger field, and the standard base-change equivalence of point groups transfers solvability.