Faithful flatness over invariants of a linearly reductive subgroup

For a geometrically reduced finite-type affine group over any field, its coordinate algebra is faithfully flat over the functions invariant under a linearly reductive closed subgroup. The subgroup need not be normal, smooth, or connected.

Exactness of invariants gives ideal contraction and hence lifts of closed points. Ambient left translations act transitively on these points; generic flatness therefore propagates to the entire invariant spectrum. Linear reductivity survives extension of the ground field, so faithful-flat descent removes the algebraic-closedness hypothesis.

The central formal inputs are ComoduleAlgebra.comap_map_coinvariants, Hilbert--Nagata finite generation, and Scheme.Hom.flat_of_transitive_closedPoints_of_finiteType.

References

• J. S. Milne, Algebraic Groups (2017), §§7 and 12.

theorem TauCeti.HopfIdeal.exists_coinvariantsLeftTranslation_comap_eq {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) [IsAlgClosed k] [Algebra.FiniteType k ↑H] [Algebra.FiniteType k ↥I.coinvariants] (hsurj : Function.Surjective (PrimeSpectrum.comap I.coinvariants.val.toRingHom)) (y z : PrimeSpectrum ↥I.coinvariants) (hy : IsClosed {y}) (hz : IsClosed {z}) : ∃ (g : WithConv (↑H →ₐ[k] k)), PrimeSpectrum.comap (↑(I.coinvariantsLeftTranslation g)).toRingHom y = z

Over an algebraically closed field, ambient left translations act transitively on closed points of a finitely generated coinvariant algebra, provided every prime of that algebra lifts to the ambient finite-type affine group.

theorem TauCeti.HopfIdeal.flat_coinvariants_of_surjective_comap {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) [IsAlgClosed k] [Algebra.FiniteType k ↑H] [IsReduced ↑H] [Algebra.FiniteType k ↥I.coinvariants] (hsurj : Function.Surjective (PrimeSpectrum.comap I.coinvariants.val.toRingHom)) : I.coinvariants.val.Flat

The coordinate algebra of a reduced finite-type affine group over an algebraically closed field is flat over a finitely generated coinvariant algebra, provided every prime of the coinvariants lifts to an ambient prime.

theorem TauCeti.HopfIdeal.faithfullyFlat_coinvariants_of_isLinearlyReductive {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] (hI : Coalgebra.IsLinearlyReductive k (↑H ⧸ I.toIdeal)) : I.coinvariants.val.FaithfullyFlat

The coordinate algebra of a geometrically reduced finite-type affine group over any field is faithfully flat over the invariants of a linearly reductive closed subgroup. The subgroup need not be normal, smooth, or connected.