Flatness of affine group morphisms

Over an algebraically closed field, an affine group morphism with finite-type source is flat if and only if it is flat at the identity. Right translation identifies the flatness conditions at rational points, and every closed point of the source is rational. No smoothness, reducedness, or finite-type hypothesis on the target is needed.

The criterion is stated using the map to the localization of the source coordinate ring. Equivalently, one can also localize the target coordinate ring at the image point, by Module.flat_iff_of_isLocalization. This is the propagation step in proving flatness of quotient morphisms: it leaves only flatness at the identity to establish.

Combined with generic freeness, it shows that a dominant homomorphism of finite-type affine groups onto a reduced group over an algebraically closed field is faithfully flat. Generic freeness makes the source coordinate ring free over a dense open subset of the target, dominance and density of rational points produce a rational source point lying over it, and translation propagates flatness from there to the identity. The source may be nonreduced, and the morphism need not be finite.

Main declarations

• TauCeti.CommHopfAlgCat.flat_iff_flat_localization_augmentation: flatness can be checked at the identity.
• TauCeti.CommHopfAlgCat.faithfullyFlat_of_dominant: a dominant homomorphism onto a reduced finite-type affine group over an algebraically closed field is faithfully flat.

References

• J. S. Milne, Algebraic Groups (2017), §5, for flatness of group homomorphisms and the translation argument, and Propositions 1.65(a) and 1.70.
• H. Matsumura, Commutative Ring Theory, Theorem 24.1, for generic freeness.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §14, for faithful flatness of dominant homomorphisms via generic flatness and translation.

theorem TauCeti.CommHopfAlgCat.flat_localization_kernel_iff {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (g : WithConv (↑K →ₐ[k] k)) : ((algebraMap (↑K) (Localization.AtPrime (RingHom.ker g.ofConv.toRingHom))).comp (↑(CommHopfAlgCat.Hom.hom f)).toRingHom).Flat ↔ ((algebraMap (↑K) (Localization.AtPrime (RingHom.ker (Bialgebra.counitAlgHom k ↑K).toRingHom))).comp (↑(CommHopfAlgCat.Hom.hom f)).toRingHom).Flat

Flatness at a rational point of the source of an affine group morphism is equivalent to flatness at the identity. No finiteness or algebraic-closedness assumption is needed.

theorem TauCeti.CommHopfAlgCat.flat_iff_flat_localization_augmentation {k : Type u} [Field k] {H K : CommHopfAlgCat k} [IsAlgClosed k] [Algebra.FiniteType k ↑K] (f : H ⟶ K) : (↑(CommHopfAlgCat.Hom.hom f)).Flat ↔ ((algebraMap (↑K) (Localization.AtPrime (RingHom.ker (Bialgebra.counitAlgHom k ↑K).toRingHom))).comp (↑(CommHopfAlgCat.Hom.hom f)).toRingHom).Flat

An affine group morphism over an algebraically closed field with finite-type source is flat exactly when its coordinate map becomes flat after localizing at the augmentation ideal of the source.

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

A dominant homomorphism from a finite-type affine group to a reduced finite-type affine group over an algebraically closed field is faithfully flat. The source may be nonreduced, and the homomorphism need not be finite.