Invariant rings of linearly reductive closed subgroups

The functions on an affine group invariant under a closed subgroup are the coinvariants of its regular comodule algebra corestricted to the subgroup. This identifies the two existing notions of coinvariants and applies Hilbert--Nagata finite generation and ideal contraction to closed subgroups. Ideal contraction implies surjectivity on prime spectra, without finite-type or reducedness assumptions.

The central inputs are ComoduleAlgebra.finiteType_coinvariants and ComoduleAlgebra.comap_map_coinvariants, which use exactness of invariants.

References

• S. Mukai, An Introduction to Invariants and Moduli (2003), §4.3.
• J. S. Milne, Algebraic Groups (2017), §12.

theorem TauCeti.HopfIdeal.coinvariants_corestrict_regular {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) : ComoduleAlgebra.coinvariants R (↑H ⧸ I.toIdeal) ↑H = I.coinvariants

Right-translation invariants are the coinvariants of the regular comodule algebra corestricted to the quotient Hopf algebra of the subgroup.

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

Invariants of a linearly reductive closed subgroup are finitely generated when the ambient affine group is of finite type.

theorem TauCeti.HopfIdeal.comap_map_coinvariants_of_isLinearlyReductive {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (hI : Coalgebra.IsLinearlyReductive k (↑H ⧸ I.toIdeal)) (J : Ideal ↥I.coinvariants) : Ideal.comap I.coinvariants.val.toRingHom (Ideal.map I.coinvariants.val.toRingHom J) = J

Every ideal of the functions invariant under a linearly reductive closed subgroup is recovered by extending it to the ambient coordinate algebra and contracting it again.

theorem TauCeti.HopfIdeal.surjective_comap_coinvariants_of_isLinearlyReductive {k : Type u} [Field k] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) (hI : Coalgebra.IsLinearlyReductive k (↑H ⧸ I.toIdeal)) : Function.Surjective (PrimeSpectrum.comap I.coinvariants.val.toRingHom)

Every point of the invariant spectrum lifts to the ambient spectrum for a linearly reductive subgroup. This does not require reducedness or finite type.