The symmetric algebra of a finite module over a Noetherian ring is Noetherian

The symmetric algebra of a finite module over a Noetherian commutative ring is Noetherian, including when the module is not free.

The hypotheses are therefore the same two that make MonoidAlgebra-style constructions Noetherian: R Noetherian and M module-finite, with no freeness and no field. The symmetric algebra is the commutative model of an enveloping algebra, and this instance is consumed in that role by TauCeti/Algebra/Lie/UniversalEnveloping/PBW/Noetherian/Basic.lean: the symmetric algebra of a Lie algebra surjects onto the associated graded of its PBW filtration, which is thereby Noetherian under the same two hypotheses.

Main results

• TauCeti.SymmetricAlgebra.instIsNoetherianRing: the symmetric algebra of a module finite over a Noetherian commutative ring is Noetherian.

References

• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Springer GTM 150 (1995), §1.4 (the Hilbert basis theorem).

instance TauCeti.SymmetricAlgebra.instIsNoetherianRing (R : Type u) (M : Type v) [CommRing R] [AddCommMonoid M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : IsNoetherianRing (SymmetricAlgebra R M)

The symmetric algebra of a module finite over a Noetherian commutative ring is Noetherian. Neither freeness of M nor a field is needed.