Hilbert series of a quotient by a homogeneous regular element

Let A be an ℕ-graded algebra over a field, with finite-dimensional graded pieces, and let f be a homogeneous non-zero-divisor of degree d. The quotient has Hilbert series Hilb(A/(f), t) = Hilb(A, t) * (1 - t^d).

The finite-dimensionality hypothesis is on the pieces, not on the whole algebra. The coefficient identity is proved over the natural numbers before passing to power series over any coefficient ring. Thus it also computes dimensions in positive characteristic; using integer coefficients retains these dimensions without reduction modulo the characteristic. Degree zero is allowed: in this case the formula asserts that every quotient piece vanishes.

These are the one-element exact-sequence formulas used to compute the Hilbert series of a quotient by a homogeneous regular sequence, in particular a coinvariant algebra presented by homogeneous basic invariants. The quotient pieces are the images of the original graded pieces under the quotient map.

Main results

• finrank_quotientPiece_span_singleton_add: the dimension identity in degrees at least d.
• finrank_quotientPiece_span_singleton_of_lt: quotienting changes no piece below d.
• mk_finrank_quotientPiece_span_singleton: the Hilbert-series identity.

References

• R. P. Stanley, Invariants of finite groups and their applications to combinatorics, Bull. Amer. Math. Soc. (N.S.) 1 (1979), §3.

The proof uses the homogeneous cancellation theorem TauCeti.GradedAlgebra.mem_of_mul_mem_add_of_isLeftRegular and the short-exact-sequence dimension formula Function.Exact.finrank_eq_add.

theorem TauCeti.GradedAlgebra.exact_mulLeft_submoduleMap_span_singleton {k : Type u_1} {A : Type u_2} [CommRing A] [CommSemiring k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (hreg : IsLeftRegular f) (n : ℕ) : Function.Exact ⇑(LinearMap.codRestrict (𝒜 (d + n)) ((LinearMap.mulLeft k f).domRestrict (𝒜 n)) ⋯) ⇑((Ideal.Quotient.mkₐ k (Ideal.span {f})).toLinearMap.submoduleMap (𝒜 (d + n)))

The degree-d + n quotient map has kernel the multiples of f from degree n, when f is homogeneous and regular.

theorem TauCeti.GradedAlgebra.finrank_quotientPiece_span_singleton_add {k : Type u_1} {A : Type u_2} [CommRing A] [Field k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (hreg : IsLeftRegular f) (n : ℕ) [Module.Finite k ↥(𝒜 (d + n))] : Module.finrank k ↥(quotientPiece 𝒜 (Ideal.span {f}) (d + n)) + Module.finrank k ↥(𝒜 n) = Module.finrank k ↥(𝒜 (d + n))

Multiplication by a homogeneous non-zero-divisor identifies the kernel of the quotient map in degree d + n with the original degree-n piece. Consequently the dimensions of the quotient degree-d + n piece and the original degree-n piece sum to the dimension of the original degree-d + n piece.

theorem TauCeti.GradedAlgebra.bijective_submoduleMap_span_singleton_of_lt {k : Type u_1} {A : Type u_2} [CommRing A] [CommSemiring k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) {n : ℕ} (hn : n < d) : Function.Bijective ⇑((Ideal.Quotient.mkₐ k (Ideal.span {f})).toLinearMap.submoduleMap (𝒜 n))

The quotient map is an isomorphism on pieces below the degree of a homogeneous relation. Regularity of the relation is not required.

theorem TauCeti.GradedAlgebra.finrank_quotientPiece_span_singleton_of_lt {k : Type u_1} {A : Type u_2} [CommRing A] [CommSemiring k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) {n : ℕ} (hn : n < d) : Module.finrank k ↥(quotientPiece 𝒜 (Ideal.span {f}) n) = Module.finrank k ↥(𝒜 n)

Quotienting by a homogeneous element of degree d does not change the dimension of any graded piece of degree less than d. Regularity is not needed here.

theorem TauCeti.GradedAlgebra.mk_finrank_quotientPiece_span_singleton {k : Type u_1} {A : Type u_2} [CommRing A] [Field k] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {f : A} {d : ℕ} {S : Type u_3} [Ring S] [∀ (n : ℕ), Module.Finite k ↥(𝒜 n)] (hf : f ∈ 𝒜 d) (hreg : IsLeftRegular f) : (PowerSeries.mk fun (n : ℕ) => ↑(Module.finrank k ↥(quotientPiece 𝒜 (Ideal.span {f}) n))) = (PowerSeries.mk fun (n : ℕ) => ↑(Module.finrank k ↥(𝒜 n))) * (1 - PowerSeries.X ^ d)

The Hilbert series of a quotient by a homogeneous non-zero-divisor of degree d is the original Hilbert series multiplied by 1 - t^d. The coefficients can be taken in any ring, including ℤ to retain dimensions in positive characteristic. No positivity hypothesis on d or connectedness hypothesis on the grading is needed.