Invariant theory

Rings of invariants of finite groups acting on commutative rings: finiteness of invariant rings and Hilbert–Poincaré series of modular invariant rings of polynomial algebras.

• Poincaré series of modular invariant rings

TheoremFiniteness over a subring containing the invariants#✓fully proved

Over a Noetherian ring R, suppose B is finite type over R and the faithful image of A in B contains every fixed element of a finite group acting on B by semiring automorphisms. Then B is finite over A and A is finite type over R.

theorem Algebra.IsInvariant.moduleFinite_and_finiteType_of_finiteType
    (R : Type*) [CommRing R] [IsNoetherianRing R]
    (A : Type*) [CommRing A] [Algebra R A]
    (B : Type*) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [FaithfulSMul A B]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [Algebra.IsInvariant A B G]
    [Algebra.FiniteType R B] :
    Module.Finite A B ∧ Algebra.FiniteType R A

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.