Extensions of geometrically solvable affine groups

Let f : H ⟶ K be a morphism of commutative Hopf algebras over a field k. Contravariantly, it represents a homomorphism from the affine group represented by K to the one represented by H. This file proves that the source group of geometric points is solvable when the target and the scheme-theoretic kernel are solvable.

On coordinate rings, the kernel has algebra

K / K·f(H⁺),

implemented as CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f). Its geometric points map injectively into those of K, with image exactly the kernel of the map induced by f. Mathlib's abstract extension theorem for solvable groups then applies directly. Conversely, a closed subgroup of a geometrically solvable affine group has solvable geometric points, so the kernel condition is also necessary once the source is solvable.

Main declarations

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty_of_kernel: geometric solvability is closed under extensions.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff_kernel: when the target is geometrically solvable, the source is geometrically solvable exactly when its kernel is.

References

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

This supplies extension closure for the "Lie--Kolchin; solvable groups" milestone in Layer 5 of the ReductiveGroups roadmap. Together with closed-subgroup and product closure, it is part of the subgroup calculus needed for the solvable radical in Layer 6.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_of_kernel (k : Type u) [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hH : geometricallySolvablePointsCommHopfAlgProperty k H) (hkernel : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f))) : geometricallySolvablePointsCommHopfAlgProperty k K

Geometric-point solvability is closed under extensions.

For the group homomorphism represented by f : H ⟶ K, assume that the target Spec H and the scheme-theoretic kernel Spec (K / K·f(H⁺)) have solvable groups of geometric points. Then the geometric point group of the source Spec K is solvable.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty_iff_kernel (k : Type u) [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hH : geometricallySolvablePointsCommHopfAlgProperty k H) : geometricallySolvablePointsCommHopfAlgProperty k K ↔ geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient K (CommHopfAlgCat.kernelHopfIdeal f))

If the target of a homomorphism is geometrically solvable, then its source is geometrically solvable exactly when its scheme-theoretic kernel is.

The forward implication is closed-subgroup stability, applied to the quotient coordinate map. The reverse implication is extension closure.