Descent of faithful flatness over coinvariants

Faithful flatness of an affine group's coordinate algebra over the functions invariant under a closed subgroup can be checked after a faithfully flat extension of the base ring. In particular, over a field the quotient-flatness problem reduces to an algebraic closure. This does not require normality, finite type, or smoothness of either group.

The coinvariant base-change equivalence identifies the inclusion of invariant functions after scalar extension with the scalar extension of the original inclusion. Faithfully flat descent then applies to that inclusion, without first equipping the coinvariants with a Hopf algebra structure. The common universe for the base rings and the coordinate algebra is required by the ring-map descent API; algebraic closure preserves that universe.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.
• TauCeti.CommHopfAlgCat.coinvariantsBaseChangeEquiv for the comparison of invariant rings.
• RingHom.CodescendsAlong.of_tensorProduct_map for descent of properties of coordinate maps.

@[simp]

theorem TauCeti.CommHopfAlgCat.faithfullyFlat_coinvariants_baseChange_iff {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) : (↑(baseChangeHopfIdeal I).coinvariants.val).FaithfullyFlat ↔ (↑I.coinvariants.val).FaithfullyFlat

Faithfully flat extension of scalars preserves and reflects faithful flatness of the coordinate algebra over its coinvariants. Thus the quotient-flatness problem over a field can be checked over an algebraic closure.