Multigraded Poincaré polynomial

DefinitionMultigraded Poincaré polynomial#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, and let \(D\) be base-change data for a multigraded free resolution \(F_\bullet\) of \(M\) in which \(F_i\) has a homogeneous basis indexed by a finite set \(\iota_i\), with \(\iota_i\) empty for every \(i > b\) for a fixed \(b \in \mathbb{N}\). The multigraded Poincaré polynomial of \(D\) is the element of the monoid algebra \(\mathbb{N}[\mathbb{N} \times \mathbb{Z}^n]\) whose coefficient at \((i, \alpha)\) is the multigraded Betti number \(\beta_{i,\alpha}(D)\) of \(D\) in homological degree \(i\) and multidegree \(\alpha\); the hypotheses on the \(\iota_i\) make these coefficients finitely supported.

MetaMathlibExt.multigradedPoincarePolynomial · 19 lines

public noncomputable def multigradedPoincarePolynomial {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι : ℕ → Type u}
    {res : MultigradedFreeResolution K n M targetGraded resolution ι}
    (data : MultigradedBaseChange targetGraded resolution ι res)
    (bound : ℕ)
    (finiteBasis : ∀ i, Finite (ι i))
    (emptyAbove : ∀ i, bound < i → IsEmpty (ι i)) :
    AddMonoidAlgebra Nat (Nat × (Fin n →₀ Int)) :=
  AddMonoidAlgebra.ofCoeff (Finsupp.ofSupportFinite (multigradedPoincareCoefficients data) (by
    have h : Function.HasFiniteSupport (multigradedPoincareCoefficients data) :=
      multigradedPoincareCoefficients_hasFiniteSupport_of_finiteResolution data
        bound finiteBasis emptyAbove
    unfold Function.HasFiniteSupport at h
    exact h))

Uses 5 · Used by 1

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded Poincaré coefficients · Finite support of the multigraded Poincaré coefficients

Used byCoefficients of the multigraded Poincaré polynomial

TheoremCoefficients of the multigraded Poincaré polynomial#✓fully proved

Let \(K\) be a field, let \(R = K[x_1, \dots, x_n]\), let \(M\) be a multigraded \(R\)-module, and let \(D\) be base-change data for a multigraded free resolution \(F_\bullet\) of \(M\) in which \(F_i\) has a homogeneous basis indexed by a finite set \(\iota_i\), with \(\iota_i\) empty for every \(i > b\) for a fixed \(b \in \mathbb{N}\). For every \(i \in \mathbb{N}\) and \(\alpha \in \mathbb{Z}^n\), the coefficient at \((i, \alpha)\) of the multigraded Poincaré polynomial of \(D\) is the multigraded Betti number \(\beta_{i,\alpha}(D)\) of \(D\) in homological degree \(i\) and multidegree \(\alpha\).

MetaMathlibExt.multigradedPoincarePolynomial_coeff · 15 lines

public theorem multigradedPoincarePolynomial_coeff {K : Type u} [Field K] {n : ℕ}
    {M : Type u} [AddCommGroup M]
    [Module (MvPolynomial (Fin n) K) M] [Module K M]
    {targetGraded : MultigradedPolynomialModule K n M}
    {resolution : CategoryTheory.ProjectiveResolution
      (ModuleCat.of (MvPolynomial (Fin n) K) M)}
    {ι : ℕ → Type u}
    {res : MultigradedFreeResolution K n M targetGraded resolution ι}
    (data : MultigradedBaseChange targetGraded resolution ι res)
    (bound : ℕ)
    (finiteBasis : ∀ i, Finite (ι i))
    (emptyAbove : ∀ i, bound < i → IsEmpty (ι i))
    (i : ℕ) (α : Fin n →₀ Int) :
    (multigradedPoincarePolynomial data bound finiteBasis emptyAbove).coeff (i, α) =
      multigradedBettiNumber data α i

Uses 8

Statement usesMultigraded base change data · Multigraded free resolution · Multigraded modules over a polynomial ring · Multigraded Betti number · Multigraded Poincaré polynomial

Proof usesMultigraded Poincaré coefficients · Multigraded Poincaré coefficients are Betti numbers · Finite support of the multigraded Poincaré coefficients

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.