Finite generation of symmetric algebras

The symmetric algebra of a finite module is a finitely generated algebra. No freeness or Noetherian hypothesis is needed. This supplies the algebraic finiteness input for the projective spectrum of a symmetric algebra.

The instances provide finite type over both the coefficient semiring and the degree-zero part. They are intended for Noetherianity of symmetric algebras and finiteness properties of their projective spectra.

instance TauCeti.SymmetricAlgebra.instFiniteType (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Algebra.FiniteType R (SymmetricAlgebra R M)

The symmetric algebra of a finite module is of finite type over the coefficient semiring, without any freeness assumption.

instance TauCeti.SymmetricAlgebra.instFiniteTypeGradeZero (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Algebra.FiniteType (↥(homogeneousSubmodule R M 0)) (SymmetricAlgebra R M)

A finite module has a symmetric algebra of finite type over its degree-zero part.