The symmetric algebra of a finite free module over a regular ring is regular #
Let M be a finite free module over a regular ring R. A basis of M identifies the symmetric
algebra Sym M with a polynomial ring over R in finitely many variables
(SymmetricAlgebra.equivMvPolynomial), which is regular
(MvPolynomial.isRegularRing_of_isRegularRing).
Over a field k this says that the polynomial functions Sym(V*) on a finite-dimensional vector
space V form a regular ring, so that their local ring at every point, in particular at the
origin, is a regular local ring. This is the regularity that descends to the invariants of a finite
group along a faithfully flat extension.
instance
TauCeti.SymmetricAlgebra.isRegularRing
(R : Type u_1)
(M : Type u_2)
[CommRing R]
[IsRegularRing R]
[AddCommMonoid M]
[Module R M]
[Module.Free R M]
[Module.Finite R M]
:
The symmetric algebra of a finite free module over a regular ring is a regular ring.