Krull dimension of the symmetric algebra of a finite free module

Let M be a finite free module over a Noetherian ring R. A basis of M identifies the symmetric algebra Sym M with a polynomial ring over R in finrank R M variables (SymmetricAlgebra.equivMvPolynomial). Transporting the corresponding facts about polynomial rings, Sym M has Krull dimension dim R + finrank R M. Over a field k this is finrank k M, and so is the height of each maximal ideal of Sym M. In particular this applies to the irrelevant ideal of elements with zero constant term, the ideal of the origin when M = V*, so the local ring of the affine space V at the origin has dimension dim V.

Main results

• TauCeti.SymmetricAlgebra.ringKrullDim_of_isNoetherianRing: over a Noetherian ring R, the symmetric algebra of a finite free module M has Krull dimension dim R + finrank R M.
• TauCeti.SymmetricAlgebra.ringKrullDim_eq_finrank: over a field k, Sym M has Krull dimension finrank k M.
• Ideal.height_symmetricAlgebra_eq_finrank_of_isMaximal: over a field k, every maximal ideal of Sym M has height finrank k M.

theorem TauCeti.SymmetricAlgebra.ringKrullDim_of_isNoetherianRing (R : Type u_1) (M : Type u_2) [CommRing R] [IsNoetherianRing R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] : ringKrullDim (SymmetricAlgebra R M) = ringKrullDim R + ↑(Module.finrank R M)

Over a Noetherian ring R, the symmetric algebra of a finite free module M has Krull dimension dim R + finrank R M.

theorem TauCeti.SymmetricAlgebra.ringKrullDim_eq_finrank (k : Type u_1) (M : Type u_2) [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] : ringKrullDim (SymmetricAlgebra k M) = ↑(Module.finrank k M)

The symmetric algebra of a finite-dimensional vector space has Krull dimension the dimension of the space.

theorem Ideal.height_symmetricAlgebra_eq_finrank_of_isMaximal {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (P : Ideal (SymmetricAlgebra k M)) [P.IsMaximal] : P.height = ↑(Module.finrank k M)

Every maximal ideal of the symmetric algebra of a finite-dimensional vector space has height the dimension of the space.