Unipotence under faithfully flat morphisms

Let f : H ⟶ K be a finite-type faithfully flat morphism of commutative Hopf algebras over a field. Contravariantly, every algebraically closed point of Spec H lifts to a point of Spec K, so geometric unipotence descends from K to H.

Unipotence is preserved when a point is precomposed with a Hopf-algebra morphism. Point lifting along f therefore transfers geometric unipotence from its source affine group to its target.

Main declaration

• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.of_faithfullyFlat: geometric unipotence descends along a finite-type faithfully flat coordinate morphism.

References

• The Stacks Project, Tags 00HQ and 00FV, for algebraically closed points of faithfully flat finite-type algebras.

This is an algebraically-closed-point bridge for Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.of_faithfullyFlat {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hfinite : (↑(CommHopfAlgCat.Hom.hom f)).FiniteType) (hflat : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) (hK : geometricallyUnipotentPointsCommHopfAlgProperty k K) : geometricallyUnipotentPointsCommHopfAlgProperty k H

Geometric unipotence descends along a finite-type faithfully flat coordinate morphism.