Surjectivity of affine group morphisms

An injective map of finite-type commutative Hopf algebras over a field induces a surjection on prime spectra. Consequently, for such a map, faithful flatness is equivalent to flatness. Neither smoothness nor reducedness is required, and the ground field need not be algebraically closed.

The spectral surjectivity theorem lifts a prime to the algebraic closure of its residue field and uses surjectivity on geometric points. This separates the surjectivity input to faithful flatness of quotient morphisms from the remaining flatness argument.

References

• J. S. Milne, Algebraic Groups (2017), §5, homomorphism theorems.

theorem TauCeti.CommHopfAlgCat.comap_surjective_of_injective {k : Type u} [Field k] {H K : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↑K] (f : H ⟶ K) (hf : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) : Function.Surjective (PrimeSpectrum.comap (↑(CommHopfAlgCat.Hom.hom f)).toRingHom)

An injective homomorphism of finite-type commutative Hopf algebras over any field induces a surjection on prime spectra.

theorem TauCeti.CommHopfAlgCat.faithfullyFlat_iff_flat_of_injective {k : Type u} [Field k] {H K : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↑K] (f : H ⟶ K) (hf : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat ↔ (↑(CommHopfAlgCat.Hom.hom f)).Flat

For an injective coordinate morphism between finite-type affine groups over a field, faithful flatness is equivalent to flatness.