Connected graded algebras that are regular at the vertex

Let A be an ℕ-graded algebra over a field k which is connected: its degree-zero part consists of the scalars. Write A₊ for the irrelevant ideal, the vertex of Spec A. If the local ring A_{A₊} is regular of dimension n, then A is a polynomial algebra over k on n homogeneous elements of positive degree.

Every element of A is a scalar modulo A₊ (TauCeti.GradedAlgebra.exists_sub_algebraMap_mem_irrelevant), so A ⧸ A₊ is k and A₊ is maximal (TauCeti.GradedAlgebra.isMaximal_toIdeal_irrelevant). Localization then identifies the cotangent space A₊ ⧸ A₊² with the cotangent space of A_{A₊} (Ideal.cotangentLocalizationEquiv), compatibly with the identification of k with the residue field. So whenever the maximal ideal of A_{A₊} is finitely generated, the cotangent space A₊ ⧸ A₊² is finite-dimensional, of dimension the minimal number of generators of that maximal ideal (IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg). In the regular case this number is n, while A has Krull dimension at least n, the dimension of its localization, and at most the dimension of its cotangent space (TauCeti.GradedAlgebra.ringKrullDim_le_finrank_cotangent). So the cotangent space has dimension exactly n, and A is a polynomial algebra on n homogeneous generators (TauCeti.GradedAlgebra.exists_bijective_aeval_of_finrank_cotangent_le).

No Noetherian hypothesis on A is needed: finite generation is a consequence.

For the invariants of a finite linear group this gives the last step of the homological proof of the Chevalley–Shephard–Todd theorem: once the invariant ring is known to be regular at its vertex, it is a polynomial algebra on homogeneous basic invariants.

Main results

• TauCeti.GradedAlgebra.finite_cotangent_of_fg: if the maximal ideal of A_{A₊} is finitely generated, the cotangent space A₊ ⧸ A₊² is finite-dimensional over k.
• TauCeti.GradedAlgebra.finrank_cotangent_le_spanFinrank: its dimension is then at most the minimal number of generators of the maximal ideal of A_{A₊}.
• TauCeti.GradedAlgebra.exists_bijective_aeval_of_isRegularLocalRing: a connected graded algebra over a field whose localization at the irrelevant ideal is a regular local ring of dimension n is a polynomial algebra on n homogeneous elements of positive degree.

References

• R. Kane, Reflection Groups and Invariant Theory, Springer (2001), § 18.
• W. Bruns, J. Herzog, Cohen–Macaulay Rings, Cambridge University Press (1993), Sections 1.5 and 2.2.

theorem TauCeti.GradedAlgebra.finite_cotangent_of_fg {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) (P : Ideal A) [P.IsPrime] (hP : P = (HomogeneousIdeal.irrelevant 𝒜).toIdeal) (hfg : (IsLocalRing.maximalIdeal (Localization.AtPrime P)).FG) : Module.Finite k (HomogeneousIdeal.irrelevant 𝒜).toIdeal.Cotangent

If the maximal ideal of the localization of a connected graded algebra at the irrelevant ideal A₊ is finitely generated, then the cotangent space A₊ ⧸ A₊² is finite-dimensional over k.

theorem TauCeti.GradedAlgebra.finrank_cotangent_le_spanFinrank {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) (P : Ideal A) [P.IsPrime] (hP : P = (HomogeneousIdeal.irrelevant 𝒜).toIdeal) (hfg : (IsLocalRing.maximalIdeal (Localization.AtPrime P)).FG) : Module.finrank k (HomogeneousIdeal.irrelevant 𝒜).toIdeal.Cotangent ≤ Submodule.spanFinrank (IsLocalRing.maximalIdeal (Localization.AtPrime P))

If the maximal ideal of the localization of a connected graded algebra at the irrelevant ideal A₊ is finitely generated, then the dimension of the cotangent space A₊ ⧸ A₊² over k is at most the minimal number of generators of that maximal ideal.

theorem TauCeti.GradedAlgebra.exists_bijective_aeval_of_isRegularLocalRing {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) (P : Ideal A) [P.IsPrime] (hP : P = (HomogeneousIdeal.irrelevant 𝒜).toIdeal) [IsRegularLocalRing (Localization.AtPrime P)] {n : ℕ} (hn : ringKrullDim (Localization.AtPrime P) = ↑n) : ∃ (f : Fin n → A), (∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ f i ∈ 𝒜 d) ∧ Function.Bijective ⇑(MvPolynomial.aeval f)

A connected graded algebra regular at its vertex is a polynomial algebra. Let A be an ℕ-graded algebra over a field k whose degree-zero part consists of the scalars. If its localization at the irrelevant ideal A₊ is a regular local ring of dimension n, then there are n homogeneous elements of positive degree f₁, …, fₙ such that k[X₁, …, Xₙ] → A, Xᵢ ↦ fᵢ, is an isomorphism.

The prime P is any prime equal to A₊, so that the statement applies to an ideal presented in another form.