Faithfully flat homomorphisms to geometrically reduced affine groups

A homomorphism between finite-type affine groups over an arbitrary field, with geometrically reduced target, is faithfully flat exactly when its coordinate map is injective. Equivalently, it is faithfully flat exactly when it is dominant. The source group may be nonreduced and the homomorphism need not be finite. These criteria establish flatness of quotient projections without assuming it as part of the input.

References

• J. S. Milne, Algebraic Groups (2017), Propositions 1.65(a) and 1.70.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §14.

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

A homomorphism between finite-type affine groups with geometrically reduced target is faithfully flat exactly when its coordinate map is injective, over any field.

theorem TauCeti.CommHopfAlgCat.faithfullyFlat_iff_dominant_of_isGeometricallyReduced {k : Type u} [Field k] {H K : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↑K] [Algebra.IsGeometricallyReduced k ↑H] (f : H ⟶ K) : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat ↔ DenseRange (PrimeSpectrum.comap (↑(CommHopfAlgCat.Hom.hom f)).toRingHom)

Dominance is equivalent to faithful flatness for a homomorphism between finite-type affine groups with geometrically reduced target. No perfection assumption on the field is needed.