Finite generation of invariants of linearly reductive groups

Let H be a linearly reductive commutative bialgebra over a field k, for instance the coordinate Hopf algebra of a linearly reductive affine group G, and let A be a finitely generated commutative k-algebra with an H-comodule algebra structure, that is, an affine k-scheme Spec A with an action of G. Then the algebra of invariants A^{co H} is a finitely generated k-algebra. This is the theorem of Hilbert and Nagata. It makes the affine quotient Spec A^{co H} a scheme of finite type. For the translation action of a linearly reductive closed subgroup N on an affine group G of finite type, it makes the invariant functions O(G)^N, the candidate coordinate ring of the homogeneous space G/N, a finitely generated algebra.

The proof follows Hilbert, with exactness of invariants (TauCeti.Comodule.Hom.exists_fixed_preimage_of_isLinearlyReductive) in place of the Reynolds operator.

• Multiplication by an invariant element is a comodule endomorphism. Lifting invariants through finitely many such morphisms shows that an invariant element of the ideal generated by invariants j₁, …, jᵣ is a combination of them with invariant coefficients: every ideal J of A^{co H} satisfies J A ∩ A^{co H} = J.
• For a finite-dimensional comodule V, the homogeneous components of an invariant of the symmetric algebra Sym V are invariant. Hilbert's argument (Subalgebra.fg_of_decompose_mem_of_comap_map_le) then shows that (Sym V)^{co H} is finitely generated.
• In general, the generators of A lie in a finite-dimensional subcomodule V, so Sym V maps onto A equivariantly. By exactness of invariants this map is onto on invariants.

No smoothness, connectedness, reducedness or characteristic assumption is made: linear reductivity is the only input. In characteristic zero, reductive groups are linearly reductive; in positive characteristic they are in general only geometrically reductive, and finite generation then needs the theorems of Nagata and Haboush instead.

Main declarations

• TauCeti.ComoduleAlgebra.mulLeftHom: multiplication by an invariant element as a comodule endomorphism.
• TauCeti.ComoduleAlgebra.comap_map_coinvariants: over a linearly reductive bialgebra, every ideal of the invariants is the contraction of the ideal it generates.
• TauCeti.ComoduleAlgebra.symmetricAlgebra: the comodule algebra structure on the symmetric algebra of a comodule.
• TauCeti.ComoduleAlgebra.fg_coinvariants_symmetricAlgebra: Hilbert's theorem, the invariants of the symmetric algebra of a finite-dimensional comodule form a finitely generated algebra.
• TauCeti.ComoduleAlgebra.finiteType_coinvariants: the invariants of a finitely generated comodule algebra form a finitely generated algebra.

References

• D. Hilbert, Über die Theorie der algebraischen Formen, Math. Ann. 36 (1890).
• M. Nagata, Invariants of a group in an affine ring, J. Math. Kyoto Univ. 3 (1964).
• S. Mukai, An Introduction to Invariants and Moduli, Cambridge University Press (2003), §4.3.
• J. S. Milne, Algebraic Groups (2017), §12.

theorem TauCeti.ComoduleAlgebra.comap_map_coinvariants {k : Type u} [Field k] {H : Type v} [Semiring H] [Bialgebra k H] {A : Type w} [CommRing A] [Algebra k A] [ComoduleAlgebra k H A] (hH : Coalgebra.IsLinearlyReductive k H) (J : Ideal ↥(coinvariants k H A)) : Ideal.comap (algebraMap (↥(coinvariants k H A)) A) (Ideal.map (algebraMap (↥(coinvariants k H A)) A) J) = J

Ideal contraction for invariants. Over a linearly reductive bialgebra, an ideal J of the invariants is recovered from the ideal of A it generates: J A ∩ A^{co H} = J.

Hilbert's finiteness theorem

theorem TauCeti.ComoduleAlgebra.fg_coinvariants_symmetricAlgebra {k : Type u} [Field k] {H : Type v} [CommSemiring H] [Bialgebra k H] (hH : Coalgebra.IsLinearlyReductive k H) (V : Type u_1) [AddCommMonoid V] [Module k V] [Comodule k H V] [Module.Finite k V] : (coinvariants k H (SymmetricAlgebra k V)).FG

Hilbert's finiteness theorem. For a finite-dimensional comodule V over a linearly reductive commutative bialgebra, the invariants of the symmetric algebra Sym V form a finitely generated algebra.

Finitely generated comodule algebras

theorem TauCeti.ComoduleAlgebra.finiteType_coinvariants {k : Type u} [Field k] {H : Type v} [CommSemiring H] [Bialgebra k H] {A : Type w} [CommRing A] [Algebra k A] [ComoduleAlgebra k H A] (hH : Coalgebra.IsLinearlyReductive k H) [Algebra.FiniteType k A] : Algebra.FiniteType k ↥(coinvariants k H A)

Finite generation of invariants. The invariants of a finitely generated commutative comodule algebra over a linearly reductive commutative bialgebra form a finitely generated algebra. Geometrically, the invariant functions on an affine scheme of finite type acted on by a linearly reductive group form a finitely generated algebra.