Points of faithfully flat affine group morphisms

Let f : H ⟶ K be a morphism of commutative Hopf algebras over a commutative ring R. Contravariantly, it represents an affine group morphism from Spec K to Spec H. If the underlying algebra map is faithfully flat and of finite type, this morphism is surjective on points valued in every algebraically closed field over R.

The algebraic point-lifting theorem is AlgHom.surjective_comp_right_of_faithfullyFlat. The result here records it in the group-valued functor-of-points API, where precomposition is the component of CommHopfAlgCat.mapPointsFunctor f.

Main declaration

• TauCeti.CommHopfAlgCat.mapPointsFunctor_app_surjective_of_faithfullyFlat: a faithfully flat finite-type coordinate morphism induces a surjection on algebraically closed points.

References

• The Stacks Project, Tag 00HQ, Lemma 10.39.16.
• The Stacks Project, Tag 00FV, Hilbert Nullstellensatz.

This is the group-valued point-lifting interface used in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. Applied to the faithfully flat morphism from an affine group onto its scheme-theoretic image, it lets properties of source points descend to all image points.

theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_app_surjective_of_faithfullyFlat {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (L : Type w) [Field L] [Algebra R L] [IsAlgClosed L] (f : H ⟶ K) (hfinite : (↑(CommHopfAlgCat.Hom.hom f)).FiniteType) (hflat : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app (CommAlgCat.of R L)))

A faithfully flat finite-type morphism of commutative Hopf algebras is surjective on points valued in an algebraically closed field.

The conclusion is stated for the component of the group-valued points functor, rather than for bare algebra maps, so it can be used directly with group-theoretic point properties.