Hilbert series of homogeneous regular-sequence quotients

For a locally finite graded algebra over a field, quotienting by a homogeneous weakly regular sequence multiplies its Hilbert series by the product of the factors 1 - t^d. The quotient pieces are the images of the original pieces in the quotient by the ideal of the whole sequence. The empty sequence and degree-zero elements are allowed.

The proof iterates mk_finrank_quotientPiece_span_singleton, using Mathlib's native RingTheory.Sequence.IsWeaklyRegular and the third isomorphism theorem to identify successive quotients with the quotient by the generated ideal. The coefficients can belong to any ring; integer coefficients preserve dimensions in every characteristic.

References

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

theorem TauCeti.GradedAlgebra.isHomogeneous_ofList {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {fs : List (A × ℕ)} (hhom : ∀ p ∈ fs, p.1 ∈ 𝒜 p.2) : Ideal.IsHomogeneous 𝒜 (Ideal.ofList (List.map Prod.fst fs))

The ideal generated by the elements of a list of homogeneous element-degree pairs is homogeneous.

theorem TauCeti.GradedAlgebra.mk_finrank_quotientPiece_of_isWeaklyRegular {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜] {S : Type u_3} [Ring S] [∀ (n : ℕ), Module.Finite k ↥(𝒜 n)] (fs : List (A × ℕ)) (hhom : ∀ p ∈ fs, p.1 ∈ 𝒜 p.2) (hreg : RingTheory.Sequence.IsWeaklyRegular A (List.map Prod.fst fs)) : (PowerSeries.mk fun (n : ℕ) => ↑(Module.finrank k ↥(quotientPiece 𝒜 (Ideal.ofList (List.map Prod.fst fs)) n))) = (PowerSeries.mk fun (n : ℕ) => ↑(Module.finrank k ↥(𝒜 n))) * (List.map (fun (p : A × ℕ) => 1 - PowerSeries.X ^ p.2) fs).prod

Quotienting by a homogeneous weakly regular sequence multiplies the Hilbert series by one factor 1 - t^d for each element. A list of element-degree pairs keeps the degrees attached to their chosen elements, including when an element is zero or has degree zero.